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.

Sign up for GitHub

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

Jump to bottom

Provide interaction id's precise range #4209

Open
ice1000 opened this issue Nov 18, 2019 · 1 comment
Open

Provide interaction id's precise range #4209

ice1000 opened this issue Nov 18, 2019 · 1 comment
Assignees
@ice1000
Labels
interaction-json JSON protocol for communicating with Agda ux: emacs Issues relating to the Emacs agda2-mode ux: interaction Issues to do with interactive development (holes, case splitting, etc)
Milestone
later

Comments

@ice1000
Copy link
Member

ice1000 commented Nov 18, 2019

We can make this in json interaction first, and then emacs (because for emacs, one will have to modify the emacs lisp files as well).

Internally there's the function getInteractionRange in Agda.TypeChecking.Monad.MetaVars that gives the source location of a hole.

There's lots of known bugs that come from Emacs not having precise enough information about source code locations (#575, #2628, #2672, #2800). If you're working on a better solution, it would be awesome if it could also be used for the Emacs mode itself :)

Originally posted by @jespercockx in #4207 (comment)
@ice1000 ice1000 added ux: interaction Issues to do with interactive development (holes, case splitting, etc) interaction-json JSON protocol for communicating with Agda ux: emacs Issues relating to the Emacs agda2-mode labels Nov 18, 2019
ice1000 added a commit to Agda-zh/agda that referenced this issue Nov 18, 2019
@ice1000
[ agda#4209 ] Json should include intervals
846a1d0
@ice1000 ice1000 mentioned this issue Nov 18, 2019
Merged
ice1000 added a commit to Agda-zh/agda that referenced this issue Nov 18, 2019
@ice1000
[ agda#4209 ] Json should include intervals
ab01556
@ice1000
Copy link
Member Author

ice1000 commented Nov 27, 2019

Status: for json interaction, the precise range is provided already.

@jespercockx jespercockx added this to the 2.6.2 milestone Dec 30, 2019
@jespercockx jespercockx modified the milestones: 2.6.2, 2.6.3 May 8, 2021
@msuperdock msuperdock mentioned this issue Mar 1, 2022
Open
@jespercockx jespercockx modified the milestones: 2.6.3, Later Aug 26, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@ice1000 ice1000

Labels
interaction-json JSON protocol for communicating with Agda ux: emacs Issues relating to the Emacs agda2-mode ux: interaction Issues to do with interactive development (holes, case splitting, etc)
Projects
None yet
Milestone
later
Development

No branches or pull requests
2 participants
@jespercockx @ice1000