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 /intf | |
| 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 'intf')
| -rw-r--r-- | intf/vernacexpr.ml | 1 |
1 files changed, 1 insertions, 0 deletions
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 |