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

Don't jump to top of file when refining an hole with a type error #113

Open
isovector opened this issue Feb 9, 2023 · 2 comments
Open
Labels
bug Something isn't working

Comments

@isovector
Copy link
Collaborator

No description provided.

@isovector isovector added the enhancement New feature or request label Feb 9, 2023
@isovector
Copy link
Collaborator Author

This appears to be caused by Agda legitimately sending a JumpToError pointing at the wrong place. However, compare the messages that agda-mode sends:

IOTCM "/home/sandy/prj/cornelis/test/Hello.agda" NonInteractive Indirect ( Cmd_goal_type_context_infer Simplified 5 (intervalsToRange (Just (mkAbsolute "/home/sandy/prj/cornelis/test/Hello.agda")) [Interval (Pn () 412 28 21) (Pn () 423 28 32)]) " slap slap " )
Agda2> agda2-info-action "*Error*" "/home/sandy/prj/cornelis/test/Hello.agda:28,27-31\n(Bool → Bool) !=< Bool\nwhen checking that the expression slap has type Bool" nil)
((last . 3) . (agda2-maybe-goto '("/home/sandy/prj/cornelis/test/Hello.agda" . 418)))

compared to cornelis:

IOTCM "/home/sandy/prj/cornelis/test/Hello.agda" NonInteractive Direct (Cmd_goal_type_context_infer Simplified 5 (intervalsToRange (Just (mkAbsolute "/home/sandy/prj/cornelis/test/Hello.agda")) [Interval (Pn () 0 28 19) (Pn () 0 28 34)]) "test slap")
{"kind":"JumpToError","filepath":"/home/sandy/prj/cornelis/test/Hello.agda","position":5}

some slight off-by-ones probably, but the important part is

Pn () 412 28 21 in the former, but Pn () 0 28 19 in the latter. It was never clear what that second argument to Pn was, but it seems to be the relative buffer-offset position of the start of the hole.

@isovector
Copy link
Collaborator Author

Unfortunately this 0 is baked pretty deeply into Pos.

Maybe a stupid fix for the time being is to not jump if the position is <50.

@isovector isovector added bug Something isn't working and removed enhancement New feature or request labels Feb 9, 2023
isovector added a commit that referenced this issue Feb 9, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
None yet
Development

No branches or pull requests

1 participant