banacorn / agda-mode-vscode

agda-mode on VS Code
https://marketplace.visualstudio.com/items?itemName=banacorn.agda-mode
MIT License
167 stars 38 forks source link

Refining a goal having `\` (instead of `λ`) results in an Internal Parse Error #175

Closed scmu closed 8 months ago

scmu commented 8 months ago

Open a file with the following text:

K : {P : Set} -> P -> P
K = {! \ x -> x  !}

Trying to refine the goal results in an Internal Parse Error. It would be fine if we replace \ by the unicode λ.

The error:

Something went wrong when parsing S-expressions. Error code: S4 "cannot read: IOTCM "FILEPATH/Bug.agda" NonInteractive Direct( Cmd_refine_or_intro False 0 (intervalsToRange (Just (mkAbsolute "FILEPATH/Bug.agda")) [Interval (Pn () 31 2 7) (Pn () 40 2 18)]) "\ x -> x" )"

agda-mode: v0.4.4 Agda version 2.6.3 (not sure what happens if I upgrade)

banacorn commented 8 months ago

Issue reproduced, thanks for reporting this!