Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Doesn't work with multiple buffers #1

Closed
isovector opened this issue Dec 29, 2021 · 5 comments
Closed

Doesn't work with multiple buffers #1

isovector opened this issue Dec 29, 2021 · 5 comments

Comments

@isovector
Copy link
Contributor

Hi there! I'm loving nvim-agda, but notice it only reliably works on the first agda buffer I open. Attempting to load agda files in other buffers does nothing, but does corrupt the syntax highlighting of the first buffer.

@jliptrap
Copy link

jliptrap commented Jan 7, 2022

This is a longstanding TODO in the README (I plan to try this plugin again once it's fixed, meanwhile it's a dealbreaker for me).

@ashinkarov
Copy link
Owner

Yes, indeed this is a well-known shortcoming, and it is mentioned in the todo. I'll try to address this, but won't make any promises on when this will become available. Meanwhile, as a workaround, one can open several vim instances.

@ashinkarov
Copy link
Owner

The latest two commits add support for having multiple files opened.

My original plan was to keep only one Agda process; feed different files and interpret the output accordingly. After studying the code of interaciton backend, it became clear that:

  1. Agda does not mark responses such as highlighting update with a filename (as it assumes only one active file per interaction)
  2. While it is possible to feed different agda file within the same interaction session, runInteraction in InteractionTop.hs would force repeated typechecking on each file change.

In essence this means that it would make more sense to fork agda process per agda file. Not sure why they don't maintain states for multiple files, but this would be a serious change in the entire interaction backend.

Let's try handling multiple files this way for now, and reconsider later, in case it will become problematic.

@mightyiam
Copy link

The readme still refers to this issue.

@ashinkarov
Copy link
Owner

@mightyiam, readme mentions this under the section named "Done", which is kind of correct. However, this might be not very intuitive and the text should move under "Features" or something.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

4 participants