[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.

5 files changed, 10 insertions, 10 deletions

diff --git a/API/API.mli b/API/API.mli
index 879323a37d..e518cf583f 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -3714,6 +3714,7 @@ sig
                    | VtProofMode of string
                    | VtQuery of vernac_part_of_script * Feedback.route_id
                    | VtBack of vernac_part_of_script * Stateid.t
+                   | VtMeta
                    | VtUnknown
    and vernac_qed_type =
      | VtKeep
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index bc7146884c..3cb1a311f8 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -503,6 +503,7 @@ type vernac_type =
   | VtProofMode of string
   | VtQuery of vernac_part_of_script * Feedback.route_id
   | VtBack of vernac_part_of_script * Stateid.t
+  | VtMeta
   | VtUnknown
 and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *)
 and vernac_start = string * opacity_guarantee * Id.t list
diff --git a/stm/stm.ml b/stm/stm.ml
index d1693519dc..0cbf72c8e6 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 158ad90846..e5d197eb17 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 2fa1e0b8dc..fe42a03a3d 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