vscoq icon indicating copy to clipboard operation
vscoq copied to clipboard

Source code location messed up in the presence of unicode characters

Open artagnon opened this issue 4 years ago • 2 comments

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})

artagnon avatar Aug 21 '20 14:08 artagnon

Does anyone have any insight on this one? The server code is much too hairy to debug, and I hope the DocumentManger fixes this.

artagnon avatar Mar 17 '21 18:03 artagnon

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?

fakusb avatar Mar 18 '21 12:03 fakusb