CoqIDE: simpler way of reopening/reclosing a proof (Close: 4168)

No "read-only" terminator.  If no terminator is present the UI
complains.  If the terminator is different, STM warns but
continues.  The STM warns that the "check the document" button
will not honor the terminator change, and what to do to avoid
that.

Technically, one cannot turn (a posteriori) an axiom into a theorem
and vice versa.  Could be done, but not with a small patch.

6 files changed, 29 insertions, 47 deletions

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index c6073d599..af728471f 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -276,21 +276,11 @@ object(self)
     Doc.focus document ~cond_top:(at start) ~cond_bot:(at stop);
     self#print_stack;
     let qed_s = Doc.tip_data document in
-    buffer#apply_tag Tags.Script.read_only
-      ~start:((buffer#get_iter_at_mark qed_s.start)#forward_find_char
-        (fun c -> not(Glib.Unichar.isspace c)))
-      ~stop:(buffer#get_iter_at_mark qed_s.stop);
     buffer#move_mark ~where:(buffer#get_iter_at_mark qed_s.stop)
       (`NAME "stop_of_input")
 
   method private exit_focus =
     Minilib.log "Unfocusing";
-    begin try
-      let { start; stop } = Doc.tip_data document in
-      buffer#remove_tag Tags.Script.read_only
-        ~start:(buffer#get_iter_at_mark start)
-        ~stop:(buffer#get_iter_at_mark stop)
-    with Doc.Empty -> () end;
     Doc.unfocus document;
     self#print_stack;
     begin try
@@ -515,7 +505,7 @@ object(self)
       | Some (start, stop) ->
         if until n start stop then begin
           ()
-        end else if start#has_tag Tags.Script.processed then begin
+        end else if stop#backward_char#has_tag Tags.Script.processed then begin
           Queue.push (`Skip (start, stop)) queue;
           loop n stop
         end else begin
@@ -563,12 +553,15 @@ object(self)
       script#recenter_insert;
       match topstack with
       | [] -> self#show_goals_aux ?move_insert ()
-      | (_,s) :: _ -> self#backtrack_to_iter (buffer#get_iter_at_mark s.start) in
+      | (_,s)::_ -> self#backtrack_to_iter (buffer#get_iter_at_mark s.start) in
     let process_queue queue =
       let rec loop tip topstack =
         if Queue.is_empty queue then conclude topstack else
         match Queue.pop queue, topstack with
-        | `Skip(start,stop), [] -> assert false
+        | `Skip(start,stop), [] ->
+            logger Pp.Error "You muse close the proof with Qed or Admitted";
+            self#discard_command_queue queue;
+            conclude [] 
         | `Skip(start,stop), (_,s) :: topstack ->
             assert(start#equal (buffer#get_iter_at_mark s.start));
             assert(stop#equal (buffer#get_iter_at_mark s.stop));
@@ -589,7 +582,7 @@ object(self)
                   Doc.assign_tip_id document id;
                   let topstack, _ = Doc.context document in
                   self#exit_focus;
-                  self#cleanup ~all:true (Doc.cut_at document tip);
+                  self#cleanup (Doc.cut_at document tip);
                   logger Pp.Notice msg;
                   self#mark_as_needed sentence;
                   if Queue.is_empty queue then loop tip []
@@ -651,7 +644,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 ~all seg =
+  method private cleanup 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 +655,6 @@ 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;
-      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 +686,13 @@ object(self)
       Coq.bind (Coq.edit_at to_id) (function
       | Good (CSig.Inl (* NewTip *) ()) ->
           if unfocus_needed then self#exit_focus;
-          self#cleanup ~all:true (Doc.cut_at document to_id);
+          self#cleanup (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 ~all:true (Doc.cut_at document tip);
+          self#cleanup (Doc.cut_at document tip);
           self#enter_focus start_id stop_id;
-          self#cleanup ~all:false (Doc.cut_at document to_id);
+          self#cleanup (Doc.cut_at document to_id);
           conclusion ()
       | Fail (safe_id, loc, msg) ->
           if loc <> None then messages#push Pp.Error "Fixme LOC";
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 87efd17d2..eb994fe8e 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1339,11 +1339,6 @@ let build_ui () =
       (Gdk.Bitmap.create_from_data ~width:2 ~height:2 "\x01\x02"));
   Tags.Script.incomplete#set_property
     (`BACKGROUND_GDK (Tags.get_processed_color ())); 
-  Tags.Script.read_only#set_property
-    (`BACKGROUND_STIPPLE
-      (Gdk.Bitmap.create_from_data ~width:2 ~height:2 "\x01\x02"));
-  Tags.Script.read_only#set_property
-    (`BACKGROUND_GDK (Tags.get_processed_color ())); 
 
   (* Showtime ! *)
   w#show ()
diff --git a/ide/session.ml b/ide/session.ml
index e0466b7e3..12b779663 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -156,8 +156,6 @@ let set_buffer_handlers
     let () = update_prev it in
     if it#has_tag Tags.Script.to_process then
       cancel_signal "Altering the script being processed in not implemented"
-    else if it#has_tag Tags.Script.read_only then
-      cancel_signal "Altering read_only text not allowed"
     else if it#has_tag Tags.Script.processed then
       call_coq_or_cancel_action (coqops#go_to_mark (`MARK text_mark))
     else if it#has_tag Tags.Script.error_bg then begin
@@ -175,8 +173,6 @@ let set_buffer_handlers
       if min_iter#equal max_iter then ()
       else if min_iter#has_tag Tags.Script.to_process then
         cancel_signal "Altering the script being processed in not implemented"
-      else if min_iter#has_tag Tags.Script.read_only then
-        cancel_signal "Altering read_only text not allowed"
       else if min_iter#has_tag Tags.Script.processed then
         call_coq_or_cancel_action (coqops#go_to_mark (`MARK text_mark))
       else if min_iter#has_tag Tags.Script.error_bg then
diff --git a/ide/tags.ml b/ide/tags.ml
index d4460b077..c9b57af4c 100644
--- a/ide/tags.ml
+++ b/ide/tags.ml
@@ -52,10 +52,6 @@ struct
     t
   let all = edit_zone :: all
   
-  let read_only = make_tag table ~name:"read_only" [`EDITABLE false;
-          `BACKGROUND !processing_color;
-          `BACKGROUND_STIPPLE_SET true ]
-
 end
 module Proof =
 struct
@@ -96,7 +92,6 @@ let set_processing_color clr =
   let s = string_of_color clr in
   processing_color := s;
   Script.incomplete#set_property (`BACKGROUND s);
-  Script.read_only#set_property (`BACKGROUND s);
   Script.to_process#set_property (`BACKGROUND s)
 
 let get_error_color () = color_of_string !error_color
diff --git a/ide/tags.mli b/ide/tags.mli
index e68015c99..14cfd0dbf 100644
--- a/ide/tags.mli
+++ b/ide/tags.mli
@@ -21,9 +21,6 @@ sig
   val tooltip : GText.tag
   val edit_zone : GText.tag (* for debugging *)
   val all : GText.tag list
-
-  (* Not part of the all list. Special tags! *)
-  val read_only : GText.tag
 end
 
 module Proof :
diff --git a/stm/stm.ml b/stm/stm.ml
index 477ca1f0d..38745e227 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -131,7 +131,7 @@ type cancel_switch = bool ref
 type branch_type =
   [ `Master
   | `Proof of proof_mode * depth
-  | `Edit of proof_mode * Stateid.t * Stateid.t ]
+  | `Edit of proof_mode * Stateid.t * Stateid.t  * vernac_qed_type ]
 type cmd_t = {
   ctac : bool; (* is a tactic, needed by the 8.4 semantics of Undo *)
   cast : ast;
@@ -449,7 +449,7 @@ end = struct (* {{{ *)
     if List.mem edit_branch (Vcs_.branches !vcs) then begin
       checkout edit_branch;
       match get_branch edit_branch with
-      | { kind = `Edit (mode, _, _) } -> Proof_global.activate_proof_mode mode
+      | { kind = `Edit (mode, _,_,_) } -> Proof_global.activate_proof_mode mode
       | _ -> assert false
     end else
       let pl = proof_nesting () in
@@ -1787,8 +1787,15 @@ let known_state ?(redefine_qed=false) ~cache id =
                 VCS.create_cluster nodes ~qed:id ~start;
                 begin match brinfo, qed.fproof with
                 | { VCS.kind = `Edit _ }, None -> assert false
-                | { VCS.kind = `Edit _ }, Some (ofp, cancel) ->
+                | { VCS.kind = `Edit (_,_,_, okeep) }, Some (ofp, cancel) ->
                     assert(redefine_qed = true);
+                    if okeep != keep then
+                      msg_error(strbrk("The command closing the proof changed. "
+                        ^"The kernel cannot take this into account and will "
+                        ^(if keep == VtKeep then "not check " else "reject ")
+                        ^"the "^(if keep == VtKeep then "new" else "incomplete")
+                        ^" proof. Reprocess the command declaring "
+                        ^"the proof's statement to avoid that."));
                     let fp, cancel =
                       Slaves.build_proof
                         ~loc ~drop_pt ~exn_info ~start ~stop ~name in
@@ -1914,7 +1921,7 @@ let finish ?(print_goals=false) () =
   VCS.print ();
   (* Some commands may by side effect change the proof mode *)
   match VCS.get_branch head with
-  | { VCS.kind = `Edit (mode, _, _) } -> Proof_global.activate_proof_mode mode
+  | { VCS.kind = `Edit (mode, _,_,_) } -> Proof_global.activate_proof_mode mode
   | { VCS.kind = `Proof (mode, _) } -> Proof_global.activate_proof_mode mode
   | _ -> ()
 
@@ -1982,7 +1989,7 @@ let merge_proof_branch ?valid ?id qast keep brname =
       VCS.delete_branch brname;
       if keep <> VtDrop then VCS.propagate_sideff None;
       `Ok
-  | { VCS.kind = `Edit (mode, qed_id, master_id) } ->
+  | { VCS.kind = `Edit (mode, qed_id, master_id, _) } ->
       let ofp =
         match VCS.visit qed_id with
         | { step = `Qed ({ fproof }, _) } -> fproof
@@ -2136,9 +2143,9 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
             | { VCS.root; kind = `Proof(_,d); pos } ->
                 VCS.delete_branch bn;
                 VCS.branch ~root ~pos bn (`Proof(mode,d))
-            | { VCS.root; kind = `Edit(_,f,q); pos } ->
+            | { VCS.root; kind = `Edit(_,f,q,k); pos } ->
                 VCS.delete_branch bn;
-                VCS.branch ~root ~pos bn (`Edit(mode,f,q)))
+                VCS.branch ~root ~pos bn (`Edit(mode,f,q,k)))
             (VCS.branches ());
           VCS.checkout_shallowest_proof_branch ();
           Backtrack.record ();
@@ -2291,13 +2298,13 @@ let edit_at id =
       | { step = `Sideff (`Ast(_,id)|`Id id) } -> id
       | { next } -> master_for_br root next in
   let reopen_branch start at_id mode qed_id tip =
-    let master_id, cancel_switch =
+    let master_id, cancel_switch, keep =
       (* Hum, this should be the real start_id in the clusted and not next *)
       match VCS.visit qed_id with
-      | { step = `Qed ({ fproof = Some (_,cs)},_) } -> start, cs
+      | { step = `Qed ({ fproof = Some (_,cs); keep },_) } -> start, cs, keep
       | _ -> anomaly (str "Cluster not ending with Qed") in
     VCS.branch ~root:master_id ~pos:id
-      VCS.edit_branch (`Edit (mode, qed_id, master_id));
+      VCS.edit_branch (`Edit (mode, qed_id, master_id, keep));
     VCS.delete_cluster_of id;
     cancel_switch := true;
     Reach.known_state ~cache:(interactive ()) id;
@@ -2324,7 +2331,7 @@ let edit_at id =
       let focused = List.exists ((=) VCS.edit_branch) (VCS.branches ()) in
       let branch_info =
         match snd (VCS.get_info id).vcs_backup with
-        | Some{ mine = _, { VCS.kind = (`Proof(m,_)|`Edit(m,_,_)) }} -> Some m
+        | Some{ mine = _, { VCS.kind = (`Proof(m,_)|`Edit(m,_,_,_)) }} -> Some m
         | _ -> None in
       match focused, VCS.cluster_of id, branch_info with
       | _, Some _, None -> assert false