agda / cornelis

agda-mode for neovim
BSD 3-Clause "New" or "Revised" License
135 stars 23 forks source link

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

Open isovector opened 1 year ago

isovector commented 1 year ago

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 commented 1 year ago

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.