High water mark incorrectly moved during undo

[lephe]

Hi! Recently I've been noticing issues with the high water mark moving after an undo.

Steps to reproduce:

• In a new file, type Definition X := 2. and step through the command.
• Change X into Y: the high water mark returns to the beginning of the file.
• Undo: the high water mark is now incorrectly back after Definition X := 2.

I suspect Sublime is undoing the region change automatically. Notice how changing X back to Y after the Steps to reproduce does not remove this incorrect highlighting, because the plugin's internal high water mark variable is correctly at the beginning of the file so the text change listener does nothing.

The following is a fairly easy, but unsatisfying fix, since you can see the high water mark jump down after then undo then up after this bit of code runs.

diff --git a/CoqPlugin.py b/CoqPlugin.py
index edfd64b..ebdcfed 100644
--- a/CoqPlugin.py
+++ b/CoqPlugin.py
@@ -843,6 +843,9 @@ def handle_view_modification(view, modification_start_index):
             text = view.substr(sublime.Region(0, worker_watermark + 1))
             worker.mark_dirty(text=text)
             worker.display.set_bad_ranges([])
+        else:
+            worker.display.set_marks(worker_watermark, worker_watermark)
+            worker.display.set_bad_ranges([])

 def check_for_terminated_views():
     for worker_key, worker in list(coq_threads.items()):

[lephe]

Aaaand of course I run into the solution on the forums just after I post this issue. There is a NO_UNDO flags for regions which can be set to avoid precisely that. I'm surprised it didn't come up earlier though, this appears to be an old option thus an old behavior...

[Calvin-L]

As far as I know, this issue has existed in the plugin since day 1. I've always kinda worked around it. (It happens to me a lot.)

Amazing that the fix is so easy. Let me know if you're working on this one; otherwise, I'll add NO_UNDO myself later this evening.

[lephe]

Excellent! Happy to help as always.