Remove STM vernaculars.

9 files changed, 19 insertions, 64 deletions

diff --git a/API/API.mli b/API/API.mli
index 901ed3528..50fbee529 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -3676,7 +3676,7 @@ sig
                    | VtProofStep of proof_step
                    | VtProofMode of string
                    | VtQuery of vernac_part_of_script * Feedback.route_id
-                   | VtStm of vernac_control * vernac_part_of_script
+                   | VtBack of vernac_part_of_script * Stateid.t
                    | VtUnknown
    and vernac_qed_type =
      | VtKeep
@@ -3685,10 +3685,6 @@ sig
    and vernac_start = string * opacity_guarantee * Names.Id.t list
    and vernac_sideff_type = Names.Id.t list
    and vernac_part_of_script = bool
-   and vernac_control =
-     | VtWait
-     | VtJoinDocument
-     | VtBack of Stateid.t
    and opacity_guarantee =
      | GuaranteesOpacity
      | Doesn'tGuaranteeOpacity
@@ -3770,7 +3766,6 @@ sig
   type option_value
   type showable
   type bullet
-  type stm_vernac
   type comment
   type register_kind
   type locatable
@@ -3922,7 +3917,6 @@ sig
   | VernacLocate of locatable
   | VernacRegister of lident * register_kind
   | VernacComments of comment list
-  | VernacStm of stm_vernac
   | VernacGoal of Constrexpr.constr_expr
   | VernacAbort of lident option
   | VernacAbortAll
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index 94e166f92..fb713d352 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -280,11 +280,6 @@ type bullet =
     | Star of int
     | Plus of int
 
-(** {6 Types concerning Stm} *)
-type stm_vernac =
-  | JoinDocument
-  | Wait
-
 (** {6 Types concerning the module layer} *)
 
 (** Rigid / flexible module signature *)
@@ -450,10 +445,6 @@ type vernac_expr =
   | VernacRegister of lident * register_kind
   | VernacComments of comment list
 
-  (* Stm backdoor: used in fake_id, will be removed when fake_ide
-     becomes aware of feedback about completed jobs. *)
-  | VernacStm of stm_vernac
-
   (* Proof management *)
   | VernacGoal of constr_expr
   | VernacAbort of lident option
@@ -504,16 +495,12 @@ type vernac_type =
   | VtProofStep of proof_step
   | VtProofMode of string
   | VtQuery of vernac_part_of_script * Feedback.route_id
-  | VtStm of vernac_control * vernac_part_of_script
+  | VtBack of vernac_part_of_script * Stateid.t
   | VtUnknown
 and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *)
 and vernac_start = string * opacity_guarantee * Id.t list
 and vernac_sideff_type = Id.t list
 and vernac_part_of_script = bool
-and vernac_control =
-  | VtWait
-  | VtJoinDocument
-  | VtBack of Stateid.t
 and opacity_guarantee =
   | GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
   | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index de98415cd..0da22fd71 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -75,10 +75,6 @@ GEXTEND Gram
       | IDENT "Local"; v = vernac_poly -> VernacLocal (true, v)
       | IDENT "Global"; v = vernac_poly -> VernacLocal (false, v)
 
-      (* Stm backdoor *)
-      | IDENT "Stm"; IDENT "JoinDocument"; "." -> VernacStm JoinDocument
-      | IDENT "Stm"; IDENT "Wait"; "." -> VernacStm Wait
-
       | v = vernac_poly -> v ]
     ]
   ;
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 5e57f5de0..51c3eb212 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -524,12 +524,6 @@ open Decl_kinds
       | VernacLocal (local, v) ->
         return (pr_locality local ++ spc() ++ pr_vernac_body v)
 
-      (* Stm *)
-      | VernacStm JoinDocument ->
-        return (keyword "Stm JoinDocument")
-      | VernacStm Wait ->
-        return (keyword "Stm Wait")
-
       (* Proof management *)
       | VernacAbortAll ->
         return (keyword "Abort All")
diff --git a/stm/stm.ml b/stm/stm.ml
index 7e17fa2f5..e0064df9b 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1049,7 +1049,7 @@ end = struct (* {{{ *)
     try
       match v with
       | VernacResetInitial ->
-          VtStm (VtBack Stateid.initial, true), VtNow
+          VtBack (true, Stateid.initial), VtNow
       | VernacResetName (_,name) ->
           let id = VCS.get_branch_pos (VCS.current_branch ()) in
           (try
@@ -1057,20 +1057,20 @@ end = struct (* {{{ *)
               fold_until (fun b (id,_,label,_,_) ->
                 if b then `Stop id else `Cont (List.mem name label))
               false id in
-            VtStm (VtBack oid, true), VtNow
+            VtBack (true, oid), VtNow
           with Not_found ->
-            VtStm (VtBack id, true), VtNow)
+            VtBack (true, id), VtNow)
       | VernacBack n ->
           let id = VCS.get_branch_pos (VCS.current_branch ()) in
           let oid = fold_until (fun n (id,_,_,_,_) ->
             if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in
-          VtStm (VtBack oid, true), VtNow
+          VtBack (true, oid), VtNow
       | VernacUndo n ->
           let id = VCS.get_branch_pos (VCS.current_branch ()) in
           let oid = fold_until (fun n (id,_,_,tactic,undo) ->
             let value = (if tactic then 1 else 0) - undo in
             if Int.equal n 0 then `Stop id else `Cont (n-value)) n id in
-          VtStm (VtBack oid, true), VtLater
+          VtBack (true, oid), VtLater
       | VernacUndoTo _
       | VernacRestart as e ->
           let m = match e with VernacUndoTo m -> m | _ -> 0 in
@@ -1087,16 +1087,16 @@ end = struct (* {{{ *)
             0 id in
           let oid = fold_until (fun n (id,_,_,_,_) ->
             if Int.equal n 0 then `Stop id else `Cont (n-1)) (n-m-1) id in
-          VtStm (VtBack oid, true), VtLater
+          VtBack (true, oid), VtLater
       | VernacAbortAll ->
           let id = VCS.get_branch_pos (VCS.current_branch ()) in
           let oid = fold_until (fun () (id,vcs,_,_,_) ->
             match Vcs_.branches vcs with [_] -> `Stop id | _ -> `Cont ())
             () id in
-          VtStm (VtBack oid, true), VtLater
+          VtBack (true, oid), VtLater
       | VernacBacktrack (id,_,_)
       | VernacBackTo id ->
-          VtStm (VtBack (Stateid.of_int id), not !Flags.batch_mode), VtNow
+          VtBack (not !Flags.batch_mode, Stateid.of_int id), VtNow
       | _ -> VtUnknown, VtNow
     with
     | Not_found ->
@@ -2484,14 +2484,8 @@ let process_transaction ?(newtip=Stateid.fresh ())
       stm_prerr_endline (fun () ->
         "  classified as: " ^ string_of_vernac_classification c);
       match c with
-      (* Joining various parts of the document *)
-      | VtStm (VtJoinDocument, b), VtNow -> join (); `Ok
-      | VtStm (VtWait, b),         VtNow -> wait (); `Ok
-      | VtStm ((VtJoinDocument|VtWait),_), VtLater ->
-          anomaly(str"classifier: join actions cannot be classified as VtLater.")
-
       (* Back *)
-      | VtStm (VtBack oid, true), w ->
+      | VtBack (true, oid), w ->
           let id = VCS.new_node ~id:newtip () in
           let { mine; others } = Backtrack.branches_of oid in
           let valid = VCS.get_branch_pos head in
@@ -2510,12 +2504,12 @@ let process_transaction ?(newtip=Stateid.fresh ())
           VCS.checkout_shallowest_proof_branch ();
           VCS.commit id (Alias (oid,x));
           Backtrack.record (); if w == VtNow then finish (); `Ok
-      | VtStm (VtBack id, false), VtNow ->
+      | VtBack (false, id), VtNow ->
           stm_prerr_endline (fun () -> "undo to state " ^ Stateid.to_string id);
           Backtrack.backto id;
           VCS.checkout_shallowest_proof_branch ();
           Reach.known_state ~cache:(interactive ()) id; `Ok
-      | VtStm (VtBack id, false), VtLater ->
+      | VtBack (false, id), VtLater ->
           anomaly(str"classifier: VtBack + VtLater must imply part_of_script.")
 
       (* Query *)
@@ -2779,8 +2773,8 @@ let query ~at ~route s =
     let clas = classify_vernac ast in
     let aast = { verbose = true; indentation; strlen; loc; expr = ast } in
     match clas with
-    | VtStm (w,_), _ ->
-       ignore(process_transaction aast (VtStm (w,false), VtNow))
+    | VtBack (_,id), _ -> (* TODO: can this still happen ? *)
+       ignore(process_transaction aast (VtBack (false,id), VtNow))
     | _ ->
        ignore(process_transaction aast (VtQuery (false, route), VtNow)))
   s
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index c2ebea961..158ad9084 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -31,8 +31,7 @@ let string_of_vernac_type = function
         Option.default "" proof_block_detection
   | VtProofMode s -> "ProofMode " ^ s
   | VtQuery (b, route) -> "Query " ^ string_of_in_script b ^ " route " ^ string_of_int route
-  | VtStm ((VtJoinDocument|VtWait), b) -> "Stm " ^ string_of_in_script b
-  | VtStm (VtBack _, b) -> "Stm Back " ^ string_of_in_script b
+  | VtBack (b, _) -> "Stm Back " ^ string_of_in_script b
 
 let string_of_vernac_when = function
   | VtLater -> "Later"
@@ -64,9 +63,6 @@ let rec classify_vernac e =
      * look at the entire dag to detect this option. *)
     | VernacSetOption (["Universe"; "Polymorphism"],_)
     | VernacUnsetOption (["Universe"; "Polymorphism"]) -> VtSideff [], VtNow
-    (* Stm *)
-    | VernacStm Wait         -> VtStm (VtWait, true), VtNow
-    | VernacStm JoinDocument -> VtStm (VtJoinDocument, true), VtNow
     (* Nested vernac exprs *)
     | VernacProgram e -> classify_vernac e
     | VernacLocal (_,e) -> classify_vernac e
@@ -79,7 +75,7 @@ let rec classify_vernac e =
     | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
         (match classify_vernac e with
         | ( VtQuery _ | VtProofStep _ | VtSideff _
-          | VtStm _ | VtProofMode _ ), _ as x -> x
+          | VtBack _ | VtProofMode _ ), _ as x -> x
         | VtQed _, _ ->
             VtProofStep { parallel = `No; proof_block_detection = None },
             VtNow
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 1602f9c68..22dc02f03 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -134,7 +134,7 @@ let rec interp_vernac sid (loc,com) =
          document. Hopefully this is fixed when VtBack can be removed
          and Undo etc... are just interpreted regularly. *)
       let is_proof_step = match fst (Vernac_classifier.classify_vernac v) with
-        | VtProofStep _ | VtStm (VtBack _, _) | VtStartProof _ -> true
+        | VtProofStep _ | VtBack (_, _) | VtStartProof _ -> true
         | _ -> false
       in
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 4fd08b42d..cfdbe43c4 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1924,7 +1924,6 @@ let interp ?proof ?loc locality poly c =
   | VernacTime _ -> assert false
   | VernacRedirect _ -> assert false
   | VernacTimeout _ -> assert false
-  | VernacStm _ -> assert false
 
   (* The STM should handle that, but LOAD bypasses the STM... *)
   | VernacAbortAll    -> CErrors.user_err  (str "AbortAll cannot be used through the Load command")
@@ -2185,10 +2184,6 @@ let interp ?(verbosely=true) ?proof (loc,c) =
   let orig_program_mode = Flags.is_program_mode () in
   let rec aux ?locality ?polymorphism isprogcmd = function
 
-    (* This assert case will be removed when fake_ide can understand
-       completion feedback *)
-    | VernacStm _ -> assert false (* Done by Stm *)
-
     | VernacProgram c when not isprogcmd -> aux ?locality ?polymorphism true c
     | VernacProgram _ -> user_err Pp.(str "Program mode specified twice")
     | VernacLocal (b, c) when Option.is_empty locality -> 
diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml
index fc11bcf4a..3cff1f14c 100644
--- a/vernac/vernacprop.ml
+++ b/vernac/vernacprop.ml
@@ -17,8 +17,7 @@ let rec is_navigation_vernac = function
   | VernacResetName _
   | VernacBacktrack _
   | VernacBackTo _
-  | VernacBack _
-  | VernacStm _ -> true
+  | VernacBack _ -> true
   | VernacRedirect (_, (_,c))
   | VernacTime (_,c) ->
       is_navigation_vernac c (* Time Back* is harmless *)