From 550da87456ae156ced70fdb123d9f36ac7b84720 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 25 Feb 2015 16:42:59 +0100
Subject: CoqIDE: correclty unfocus (remove all tags) when jumping out of a
 proof

---
 ide/coqOps.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'ide')

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 8ba1c8ecd2..1800cb8fe8 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -662,10 +662,14 @@ object(self)
       buffer#remove_tag Tags.Script.unjustified ~start ~stop;
       buffer#remove_tag Tags.Script.tooltip ~start ~stop;
       buffer#remove_tag Tags.Script.to_process ~start ~stop;
+      buffer#remove_tag Tags.Script.read_only ~start ~stop;
+      buffer#remove_tag Tags.Script.error ~start ~stop;
+      buffer#remove_tag Tags.Script.error_bg ~start ~stop;
       buffer#move_mark ~where:start (`NAME "start_of_input")
     end;
     List.iter (fun { start } -> buffer#delete_mark start) seg;
-    List.iter (fun { stop } -> buffer#delete_mark stop) seg
+    List.iter (fun { stop } -> buffer#delete_mark stop) seg;
+    self#print_stack
 
   (** Wrapper around the raw undo command *)
   method private backtrack_to_id ?(move_insert=true) (to_id, unfocus_needed) =
-- 
cgit v1.2.3