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.mli | |
| 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.mli')
| -rw-r--r-- | stm/vernac_classifier.mli | 3 |
1 files changed, 0 insertions, 3 deletions
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 |