diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-10-15 19:21:00 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-10-17 02:18:29 +0200 |
| commit | ab915f905ca81018521db63cdd0f3126b35c69c6 (patch) | |
| tree | 89846b34951330cdb4dcabaaad9d715afbb74173 /stm/vernac_classifier.ml | |
| parent | c00cecfc66eb76d6bca8980ef719577fd81cc400 (diff) | |
[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.
Diffstat (limited to 'stm/vernac_classifier.ml')
| -rw-r--r-- | stm/vernac_classifier.ml | 8 |
1 files changed, 3 insertions, 5 deletions
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 _ |