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

Syntax is lost after go-to-def (or editing a file) #117

Open
4e554c4c opened this issue Apr 5, 2023 · 8 comments
Open

Syntax is lost after go-to-def (or editing a file) #117

4e554c4c opened this issue Apr 5, 2023 · 8 comments

Comments

@4e554c4c
Copy link
Collaborator

4e554c4c commented Apr 5, 2023

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
Copy link
Collaborator

I can't reproduce this

@4e554c4c
Copy link
Collaborator Author

@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

@isovector
Copy link
Collaborator

https://asciinema.org/a/TwY5W0vbjBYKh1iOdHckHiwEO this is the functionality on my end

@dolio
Copy link

dolio commented Oct 28, 2024

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.

@4e554c4c
Copy link
Collaborator Author

@isovector could we re-open this since we have more people seeing the issue?

@isovector isovector reopened this Nov 22, 2024
@isovector
Copy link
Collaborator

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!

@4e554c4c
Copy link
Collaborator Author

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

@isovector
Copy link
Collaborator

I'm all for it if someone is willing to make the introduction

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

3 participants