Merge PR #1055: Remove STM vernaculars

3 files changed, 19 insertions, 26 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index 3386044f26..e0064df9bb 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 ->
@@ -2373,6 +2373,7 @@ let finish () =
   | _ -> ()
 
 let wait () =
+  finish ();
   Slaves.wait_all_done ();
   VCS.print ()
 
@@ -2386,7 +2387,6 @@ let rec join_admitted_proofs id =
   | _ -> join_admitted_proofs view.next
 
 let join () =
-  finish ();
   wait ();
   stm_prerr_endline (fun () -> "Joining the environment");
   Global.join_safe_environment ();
@@ -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 -> finish (); 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/stm.mli b/stm/stm.mli
index 188b176bab..3f01fca013 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -51,6 +51,9 @@ val edit_at : Stateid.t -> [ `NewTip | `Focus of focus ]
 (* Evaluates the tip of the current branch *)
 val finish : unit -> unit
 
+(* Internal use (fake_ide) only, do not use *)
+val wait : unit -> unit
+
 val observe : Stateid.t -> unit
 
 val stop_worker : string -> unit
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index c2ebea961f..158ad90846 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