From ab915f905ca81018521db63cdd0f3126b35c69c6 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 15 Oct 2017 19:21:00 +0200 Subject: [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. --- stm/stm.ml | 7 +++++-- stm/vernac_classifier.ml | 8 +++----- stm/vernac_classifier.mli | 3 --- 3 files changed, 8 insertions(+), 10 deletions(-) (limited to 'stm') 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 -- cgit v1.2.3