isovector
Syntax is lost after go-to-def (or editing a file)
After loading an agda file, and opening another file with :CornelisGoToDefinition, the syntax information in the original agda file is lost and goto def will no longer work.
This appears to also occur if an agda file is opened (e.g. through :e).
@isovector have you verified that go-to def is working? The file still appears to be loaded (it is colored) but actions do not work
https://asciinema.org/a/TwY5W0vbjBYKh1iOdHckHiwEO this is the functionality on my end
Perhaps a step was left out of the original description.
If I jump to a file, load that file, then jump back, the information seems gone from the original file. E.G. trying to immediately do the same jump just says "No syntax under cursor."
I would guess it's because information for only one file is loaded at a time? So loading the second file replaces the first? And possibly that's by design. I just thought I'd leave information on how to (possibly) reproduce the situation.
@isovector could we re-open this since we have more people seeing the issue?
For what it's worth, this project is mostly unmaintained these days, since I'm no longer actively using Agda and surprisingly busy at work!
makes sense. maybe it would make sense to transfer control of this repo to an organization (they usually have better long-term maintainership ability, since you can have multiple owners)
i wonder if the agda organization would be able to host cornelis