[stm] Remove VtBack from public classification.

We interpret meta-commands directly, instead of going by an
intermediate "classifier step".

The code could still use some further refactoring, in particular, the
`part_of_script` bit is a bit strange likely coming from some special
treatment of `VtMeta` in the `query` call, and should go away.

2 files changed, 48 insertions, 46 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index 0cbf72c8e..b974d319e 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1036,8 +1036,8 @@ module Backtrack : sig
   (* we could navigate the dag, but this ways easy *)
   val branches_of : Stateid.t -> backup
 
-  (* To be installed during initialization *)
-  val undo_vernac_classifier : vernac_expr -> vernac_classification
+  (* Returns the state that the command should backtract to *)
+  val undo_vernac_classifier : vernac_expr -> Stateid.t * vernac_when
 
 end = struct (* {{{ *)
 
@@ -1105,7 +1105,7 @@ end = struct (* {{{ *)
     try
       match v with
       | VernacResetInitial ->
-          VtBack (true, Stateid.initial), VtNow
+          Stateid.initial, VtNow
       | VernacResetName (_,name) ->
           let id = VCS.get_branch_pos (VCS.current_branch ()) in
           (try
@@ -1113,20 +1113,20 @@ end = struct (* {{{ *)
               fold_until (fun b (id,_,label,_,_) ->
                 if b then `Stop id else `Cont (List.mem name label))
               false id in
-            VtBack (true, oid), VtNow
+            oid, VtNow
           with Not_found ->
-            VtBack (true, id), VtNow)
+            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
-          VtBack (true, oid), VtNow
+          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
-          VtBack (true, oid), VtLater
+          oid, VtLater
       | VernacUndoTo _
       | VernacRestart as e ->
           let m = match e with VernacUndoTo m -> m | _ -> 0 in
@@ -1143,17 +1143,17 @@ 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
-          VtBack (true, oid), VtLater
+          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
-          VtBack (true, oid), VtLater
+          oid, VtLater
       | VernacBacktrack (id,_,_)
       | VernacBackTo id ->
-          VtBack (VCS.is_interactive () = `Yes, Stateid.of_int id), VtNow
-      | _ -> VtUnknown, VtNow
+          Stateid.of_int id, VtNow
+      | _ -> anomaly Pp.(str "incorrect VtMeta classification")
     with
     | Not_found ->
        CErrors.user_err ~hdr:"undo_vernac_classifier"
@@ -2577,7 +2577,38 @@ let snapshot_vio ~doc ldir long_f_dot_vo =
 let reset_task_queue = Slaves.reset_task_queue
 
 (* Document building *)
-let rec process_transaction ?(newtip=Stateid.fresh ())
+let process_back_meta_command ~part_of_script ~newtip ~head oid aast w =
+  match part_of_script, w with
+  | true, 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
+    List.iter (fun branch ->
+        if not (List.mem_assoc branch (mine::others)) then
+          ignore(merge_proof_branch ~valid aast VtDrop branch))
+      (VCS.branches ());
+    VCS.checkout_shallowest_proof_branch ();
+    let head = VCS.current_branch () in
+    List.iter (fun b ->
+        if not(VCS.Branch.equal b head) then begin
+          VCS.checkout b;
+          VCS.commit (VCS.new_node ()) (Alias (oid,aast));
+        end)
+      (VCS.branches ());
+    VCS.checkout_shallowest_proof_branch ();
+    VCS.commit id (Alias (oid,aast));
+    Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok
+
+  | false, VtNow ->
+    stm_prerr_endline (fun () -> "undo to state " ^ Stateid.to_string oid);
+    Backtrack.backto oid;
+    VCS.checkout_shallowest_proof_branch ();
+    Reach.known_state ~cache:(VCS.is_interactive ()) oid; `Ok
+
+  | false, VtLater ->
+    anomaly(str"undo classifier: VtMeta + VtLater must imply part_of_script.")
+
+let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true)
   ({ verbose; loc; expr } as x) c =
   stm_pperr_endline (fun () -> str "{{{ processing: " ++ pr_ast x);
   let vcs = VCS.backup () in
@@ -2590,36 +2621,8 @@ let rec process_transaction ?(newtip=Stateid.fresh ())
       match c with
       (* Meta *)
       | VtMeta, _ ->
-        let clas = Backtrack.undo_vernac_classifier expr in
-        process_transaction ~newtip x clas
-      (* Back *)
-      | 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
-          List.iter (fun branch ->
-            if not (List.mem_assoc branch (mine::others)) then
-              ignore(merge_proof_branch ~valid x VtDrop branch))
-            (VCS.branches ());
-          VCS.checkout_shallowest_proof_branch ();
-          let head = VCS.current_branch () in
-          List.iter (fun b ->
-            if not(VCS.Branch.equal b head) then begin
-              VCS.checkout b;
-              VCS.commit (VCS.new_node ()) (Alias (oid,x));
-            end)
-            (VCS.branches ());
-          VCS.checkout_shallowest_proof_branch ();
-          VCS.commit id (Alias (oid,x));
-          Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok
-      | 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:(VCS.is_interactive ()) id; `Ok
-      | VtBack (false, id), VtLater ->
-          anomaly(str"classifier: VtBack + VtLater must imply part_of_script.")
-
+        let id, w = Backtrack.undo_vernac_classifier expr in
+        process_back_meta_command ~part_of_script ~newtip ~head id x w
       (* Query *)
       | VtQuery (false, route), VtNow ->
         begin
@@ -2881,8 +2884,8 @@ let query ~doc ~at ~route s =
     let clas = classify_vernac ast in
     let aast = { verbose = true; indentation; strlen; loc; expr = ast } in
     match clas with
-    | VtBack (_,id), _ -> (* TODO: can this still happen ? *)
-       ignore(process_transaction aast (VtBack (false,id), VtNow))
+    | VtMeta , _ -> (* TODO: can this still happen ? *)
+       ignore(process_transaction ~part_of_script:false aast (VtMeta,VtNow))
     | _ ->
        ignore(process_transaction aast (VtQuery (false, route), VtNow)))
   s
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index e5d197eb1..3aa2cd707 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -31,7 +31,6 @@ 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
-  | VtBack (b, _) -> "Stm Back " ^ string_of_in_script b
   | VtMeta -> "Meta "
 
 let string_of_vernac_when = function
@@ -73,7 +72,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 _
-          | VtBack _ | VtProofMode _ | VtMeta), _ as x -> x
+          | VtProofMode _ | VtMeta), _ as x -> x
         | VtQed _, _ ->
             VtProofStep { parallel = `No; proof_block_detection = None },
             VtNow