diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-03-28 11:23:50 +0200 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-03-28 11:23:50 +0200 |
commit | acf5e4b0a7bae99263f76e7330fd85c56c4eda68 (patch) | |
tree | 58b9289d5cc0d87b78b9f19ad3124c548915344e /ide | |
parent | 792042a695083b73f0e998b20197ef0d3de25812 (diff) |
coqide: avoid marking sentences that are not in the document anymore
Diffstat (limited to 'ide')
-rw-r--r-- | ide/coqOps.ml | 6 |
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 |