coqide: use Document instead of tags to detect sentences to `Skip (#4829)

When one jumps from a focused area to a point after the focused zone,
sentences that are already processed (in the Doc.context of the focused
area) have not to be processed again (they are tagged as `Skip).

Detection of such sentences was based on tags (i.e. colors) that is shaky.
Now we use the sentence-marks as stored in the document data structure.

1 files changed, 7 insertions, 1 deletions

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 5b6bad349..741a1d6e2 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -561,13 +561,19 @@ object(self)
       condition returns true; it is fed with the number of phrases read and the
       iters enclosing the current sentence. *)
   method private fill_command_queue until queue =
+    let topstack =
+      if Doc.focused document then fst (Doc.context document) else [] in
     let rec loop n iter =
       match Sentence.find buffer iter with
       | None -> ()
       | Some (start, stop) ->
         if until n start stop then begin
           ()
-        end else if stop#backward_char#has_tag Tags.Script.processed then begin
+        end else if
+          List.exists (fun (_, s) ->
+            start#equal (buffer#get_iter_at_mark s.start) &&
+            stop#equal (buffer#get_iter_at_mark s.stop)) topstack
+        then begin
           Queue.push (`Skip (start, stop)) queue;
           loop n stop
         end else begin