vscoq
vscoq copied to clipboard
Source code location messed up in the presence of unicode characters
A recent example of this:
❯ coqc Cubical.v
File "./Cubical.v", line 84, characters 44-45:
...
vscoq displays the error in line 86, characters 15-16. Here are lines 82 through 88:
(rew uniq in sublayer (Hp := Hp) (↑ (Hr ↕ Hq)) ε' b)) =
sublayer (Hp := Hp) (Hr ↕ Hq) ε'
(sublayer (Hp := Hp ↕ Hr) (↑ Hq) ε b);
cohcube {n' p q r} {Hn' : S (S n') <= n} {Hp : p <= r}
{Hr : r <= q} {Hq : q <= n'}
(ε : side) (ε' : side) {D : csp Hn'}
(E : box (le_n (S (S n'))) D -> Type@{l})
Does anyone have any insight on this one? The server code is much too hairy to debug, and I hope the DocumentManger fixes this.
The code that is currently in use for this will be thrown away with the new Document manager. I looked at the current code, but I've no good insight why this is screwed up.
Note that #181 screwed up the part that adjusts code positions after editing (which was already a but less broken before) as a trade-of. So It could be the case that reloading the file fixes the position.
I by myself have noticed wrong columns before, but I do not expect wrong lines to persist after reloading the file, can you confirm the later?