search

coq-community / vscoq

A Visual Studio Code extension for Coq [maintainers=@rtetley,@huynhtrankhanh,@thery,@Blaisorblade]
MIT License
330 stars 68 forks source link

Bug in the computation of "next sentence" #843

Open gares opened 1 month ago

gares commented 1 month ago

After an editing session

Lemma bar ...
Edited Tactic.
Search bla bla.

Lemma foo ...

the document state gets printed fine, but the calculation of the next sentence is off, in particular Edited Tactic and Search ... are "glued".

We should check which data structure (the id -> sentence map or the end_offset -> sentence map) is used to compute the next sentence, and if the bug is in the code updating the data structure or the code computing the next sentence. The first data structure seems correct when printed.

gares commented 1 month ago

CC @thery

This is the bug we have been discussing in the last days. The exec state seems fine. But the navigation commands don't work as expected.