aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coqOps.ml
diff options
context:
space:
mode:
authorGravatar gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-10-24 15:41:37 +0000
committerGravatar gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-10-24 15:41:37 +0000
commit7bded288b7727625ee353af5a142ecba15d57240 (patch)
tree843bedb30c5b7c9bf86ae762a93d57102ab6f0f2 /ide/coqOps.ml
parent62e3d6b5f71d17fd4ef683d9f36461d9d16b1a6c (diff)
CoqIDE: fix coloring bug when jumping back to the first phrase
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16928 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coqOps.ml')
-rw-r--r--ide/coqOps.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index eb09d3bbb..59c399842 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -553,7 +553,8 @@ object(self)
(* finds the state_id and if it an unfocus is needed to reach it *)
method private find_id until =
- try Doc.find_id document (fun id { start;stop } -> until (Some id) start stop)
+ try
+ Doc.find_id document (fun id { start;stop } -> until (Some id) start stop)
with Not_found -> initial_state, Doc.focused document
method private cleanup seg =
@@ -586,6 +587,7 @@ object(self)
buffer#remove_tag Tags.Script.tooltip ~start ~stop;
buffer#remove_tag Tags.Script.processed ~start ~stop;
buffer#remove_tag Tags.Script.to_process ~start ~stop;
+ buffer#remove_tag Tags.Script.unjustified ~start ~stop;
self#show_goals in
Coq.bind (Coq.lift opening) (fun () ->
let rec undo to_id unfocus_needed =