Merge PR #7096: coqide: avoid marking sentences that are not in the document anymore

1 files changed, 6 insertions, 0 deletions

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 78fbce5c8..6c3438a4b 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -362,7 +362,12 @@ object(self)
     let query = Coq.query (route_id,(phrase,sid)) in
     Coq.bind (Coq.seq action query) next
 
+  method private still_valid { edit_id = id } =
+    try ignore(Doc.find_id document (fun _ { edit_id = id1 } -> id = id1)); true
+    with Not_found -> false
+
   method private mark_as_needed sentence =
+   if self#still_valid sentence then begin
     Minilib.log_pp Pp.(str "Marking " ++ dbg_to_string buffer false None sentence);
     let start = buffer#get_iter_at_mark sentence.start in
     let stop = buffer#get_iter_at_mark sentence.stop in
@@ -383,6 +388,7 @@ object(self)
     in
     List.iter (fun t -> buffer#remove_tag t ~start ~stop) all_tags;
     List.iter (fun t -> buffer#apply_tag t ~start ~stop) tags
+   end
 
   method private attach_tooltip ?loc sentence text =
     let start_sentence, stop_sentence, phrase = self#get_sentence sentence in