search

coq-community / vscoq

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

vscoq 2.1.3, break seems broken #803

Open thery opened 2 weeks ago

thery commented 2 weeks ago

Here is my example

Goal forall A B C D E F : Prop, A -> B -> C -> D -> E -> F -> A.
Proof.
intros A B C D E F.
intros HA; intros HB; intros HC; intros HD; intros HE; intros HF; exact HA.
Qed.

if I execute everything ddd1 if I try to break the line after HE; The interface goes into an inconsistent state ddd2

gares commented 2 weeks ago

I think the range stuff was not invalidated since the document is not. The code did detect that the texts parses to the same token list, so no need to recompute. But since the new text is different in length/number-of-lines, the highlighting state needs to be invalidated hence recomputed.

gares commented 2 weeks ago

The colors did not move at all, this is why I'm giving this analysis of the bug.