CoqIDE: do not lose tag on Qed ending focused proof

1 files changed, 6 insertions, 6 deletions

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 1800cb8fe..6f8305afe 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -589,7 +589,7 @@ object(self)
                   Doc.assign_tip_id document id;
                   let topstack, _ = Doc.context document in
                   self#exit_focus;
-                  self#cleanup (Doc.cut_at document tip);
+                  self#cleanup ~all:true (Doc.cut_at document tip);
                   logger Pp.Notice msg;
                   self#mark_as_needed sentence;
                   if Queue.is_empty queue then loop tip []
@@ -651,7 +651,7 @@ object(self)
       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 =
+  method private cleanup ~all seg =
     if seg <> [] then begin
       let start = buffer#get_iter_at_mark (CList.last seg).start in
       let stop = buffer#get_iter_at_mark (CList.hd seg).stop in
@@ -662,7 +662,7 @@ 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;
+      if all then 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")
@@ -694,13 +694,13 @@ object(self)
       Coq.bind (Coq.edit_at to_id) (function
       | Good (CSig.Inl (* NewTip *) ()) ->
           if unfocus_needed then self#exit_focus;
-          self#cleanup (Doc.cut_at document to_id);
+          self#cleanup ~all:true (Doc.cut_at document to_id);
           conclusion ()
       | Good (CSig.Inr (* Focus  *) (stop_id,(start_id,tip))) ->
           if unfocus_needed then self#exit_focus;
-          self#cleanup (Doc.cut_at document tip);
+          self#cleanup ~all:true (Doc.cut_at document tip);
           self#enter_focus start_id stop_id;
-          self#cleanup (Doc.cut_at document to_id);
+          self#cleanup ~all:false (Doc.cut_at document to_id);
           conclusion ()
       | Fail (safe_id, loc, msg) ->
           if loc <> None then messages#push Pp.Error "Fixme LOC";