Interaction holes appearing in wrong place

[DrNico]

Here's an interesting bug. Commented lines ending with a dash cause subsequent interaction holes to appear in the wrong place, thereby causing mayhem with the file contents.

Example source code causing the problem:

data Nat : Set where
    zero    : Nat
    succ    : Nat → Nat

{- line ending with dash -
-}

plus : Nat → Nat → Nat
plus zero n     = ?
plus (succ m) n = plus m (succ n)

Then load (^c - ^l) and watch the hole overwriting and pushing text around.

Setup is:

• agda-mode 0.7.12
• language-agda 1.0.2, tree-sitter is NOT enabled

[banacorn]

Issue reproduced!

I believe this has something to do with "hole finding": https://github.com/banacorn/agda-mode/blob/master/src/parser/hole.ts

The parsing is now done with some awful regular expressions, an ugly patch should fix it.

Hope that the parsing can be done in CFG in the future (with tree-sitter), or perhaps we can do away with parsing completely by having a better interface with agda.