search

Calvin-L / sublime-coq-plugin

Syntax highlighting and Coq interactivity for Sublime Text 3
MIT License
6 stars 4 forks source link

Water mark does not always go up after editing stepped code #9

Closed lephe closed 1 year ago

lephe commented 1 year ago

In some cases, mostly after getting a Coq error after trying to step a statement, editing stepped code will not move the water mark back up.

Steps to reproduce :

  1. Input the following code
About id.
Definition idT: Type -> Type := id.
  1. Step About id (which succeeds), then step the definition for idT (which fails because id only works at Type 0).
  2. Notice the water mark stays at the end of the first line (at offset 9), as expected.
  3. Add a character to the first line to change it into About id2.
  4. If the bug triggered, the water mark is now still on the first line.
  5. Additionally, stepping down again sends coqtop a dot (the new character at offset 9).

It doesn't happen all the time... I tried to debug it by changing the logger to print to the console, and it went away. I'm suspecting maybe some async/delay issues?

(I'm back at it and may have a PR or two coming, hopefully that helps!)

Calvin-L commented 1 year ago

I was able to reproduce this right away. For me, it happens 100% of the time with

  1. make a new file
  2. set the syntax to Coq
  3. (follow instructions above)

It seems that CoqTextChangeListener.is_applicable is called after step (1), and then never again. It returns False because the file is not a Coq file at that time. Then, the plugin cannot respond to text change events.

I don't have a fix in mind yet.

Calvin-L commented 1 year ago

I've thought about it and I have two possible fixes in mind.

  1. Just let CoqTextChangeListener run on every buffer. This should be very cheap, but it is philosophically unsatisfying.
  2. Manage CoqTextChangeListener by hand. They can be manually attached and detached from buffers. Done right, this would let us bypass any weirdness about is_applicable and know for sure that there is a CoqTextChangeListener attached to every buffer that has a background worker.

I'm not a fan of the mess that option 2 creates, but it is the one I'm leaning toward.

lephe commented 1 year ago

Quick remark: shouldn't a ViewEventListener be able to detect a change in syntax settings and then instantiate/attach a listener on the associated buffer if the syntax was set to Coq but no listener was present?

Calvin-L commented 1 year ago

I've pushed a simple fix for now and filed a bug report upstream. We can come back to this if "listening to every change on every buffer" proves too costly.