diff options
| -rw-r--r-- | API/API.mli | 1 | ||||
| -rw-r--r-- | intf/vernacexpr.ml | 1 | ||||
| -rw-r--r-- | stm/stm.ml | 7 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 8 | ||||
| -rw-r--r-- | stm/vernac_classifier.mli | 3 |
5 files changed, 10 insertions, 10 deletions
diff --git a/API/API.mli b/API/API.mli index 879323a37..e518cf583 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 bc7146884..3cb1a311f 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 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 |