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/stm.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/stm.ml')
| -rw-r--r-- | stm/stm.ml | 7 |
1 files changed, 5 insertions, 2 deletions
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 |