[stm] First step to move interpretation of Undo commands out of the classifier.

The vernacular classifier has a current special case for "Undo" like
commands, as it needs access to the document structure in order to
produce the proper "VtBack" classification, however the classifier is
defined before the document is.

We introduce a new delegation status `VtMeta` that allows us to
interpreted such commands outside the classifier itself.

3 files changed, 8 insertions, 10 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index d1693519d..0cbf72c8e 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2414,7 +2414,6 @@ let new_doc { doc_type ; require_libs } =
   State.restore_root_state ();
 
   let doc = VCS.init doc_type Stateid.initial in
-  set_undo_classifier Backtrack.undo_vernac_classifier;
 
   begin match doc_type with
   | Interactive ln ->
@@ -2578,7 +2577,7 @@ let snapshot_vio ~doc ldir long_f_dot_vo =
 let reset_task_queue = Slaves.reset_task_queue
 
 (* Document building *)
-let process_transaction ?(newtip=Stateid.fresh ())
+let rec process_transaction ?(newtip=Stateid.fresh ())
   ({ verbose; loc; expr } as x) c =
   stm_pperr_endline (fun () -> str "{{{ processing: " ++ pr_ast x);
   let vcs = VCS.backup () in
@@ -2589,6 +2588,10 @@ let process_transaction ?(newtip=Stateid.fresh ())
       stm_prerr_endline (fun () ->
         "  classified as: " ^ string_of_vernac_classification c);
       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
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 158ad9084..e5d197eb1 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -32,6 +32,7 @@ let string_of_vernac_type = function
   | 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
   | VtLater -> "Later"
@@ -53,9 +54,6 @@ let make_polymorphic (a, b as x) =
       VtStartProof (x, Doesn'tGuaranteeOpacity, ids), b
   | _ -> x
 
-let undo_classifier = ref (fun _ -> assert false)
-let set_undo_classifier f = undo_classifier := f
-
 let rec classify_vernac e =
   let static_classifier e = match e with
     (* Univ poly compatibility: we run it now, so that we can just
@@ -75,7 +73,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 _ ), _ as x -> x
+          | VtBack _ | VtProofMode _ | VtMeta), _ as x -> x
         | VtQed _, _ ->
             VtProofStep { parallel = `No; proof_block_detection = None },
             VtNow
@@ -191,7 +189,7 @@ let rec classify_vernac e =
     | VernacBack _ | VernacAbortAll
     | VernacUndoTo _ | VernacUndo _
     | VernacResetName _ | VernacResetInitial
-    | VernacBacktrack _ | VernacBackTo _ | VernacRestart -> !undo_classifier e
+    | VernacBacktrack _ | VernacBackTo _ | VernacRestart -> VtMeta, VtNow
     (* What are these? *)
     | VernacToplevelControl _
     | VernacRestoreState _
diff --git a/stm/vernac_classifier.mli b/stm/vernac_classifier.mli
index 2fa1e0b8d..fe42a03a3 100644
--- a/stm/vernac_classifier.mli
+++ b/stm/vernac_classifier.mli
@@ -18,9 +18,6 @@ val classify_vernac : vernac_expr -> vernac_classification
 val declare_vernac_classifier :
   Vernacexpr.extend_name -> (raw_generic_argument list -> unit -> vernac_classification) -> unit
 
-(** Set by Stm *)
-val set_undo_classifier : (vernac_expr -> vernac_classification) -> unit
-
 (** Standard constant classifiers *)
 val classify_as_query : vernac_classification
 val classify_as_sideeff : vernac_classification