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

Correctly pass ranges to Agda when operating over IPs #97

Open
2 of 3 tasks
isovector opened this issue Nov 22, 2022 · 3 comments
Open
2 of 3 tasks

Correctly pass ranges to Agda when operating over IPs #97

isovector opened this issue Nov 22, 2022 · 3 comments
Labels
question Further information is requested

Comments

@isovector
Copy link
Owner

isovector commented Nov 22, 2022

The Agda interface needs a lot of love here:

  1. Mangle Ranges into the right representation for over the wire
  2. Attach buffer offsets to the ranges. I think we can get these via:
function! FileOffset()
    return line2byte(line('.')) + col('.') - 1
endfunction
  1. More correctly track IPs. These currently have an interval attached to them, but a better way would be to track them in extmarks.
@isovector
Copy link
Owner Author

To do the extmarks stuff, we'll need a map from interaction points to their extmarks. And then check whether nvim_buf_get_extmark_by_id with the details option correctly gives back the ending of its extmark after editing.

@isovector isovector added the question Further information is requested label Jan 26, 2023
@isovector
Copy link
Owner Author

This might now be fixed by @Lysxia's new patch.

@Lysxia
Copy link
Contributor

Lysxia commented Jan 26, 2023

Right, the "attach buffer offsets" task seems to be subsumed by the new ability to convert between the two kinds of offsets at will.

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

No branches or pull requests

2 participants