diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-11-23 11:38:55 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-20 16:52:43 +0100 |
| commit | 28d45c2413ad24c758fca5cfb00ec4ba20935f39 (patch) | |
| tree | 50f60424aac3c9e898bb9f9192416c58f44aa7b6 /toplevel/vernac.ml | |
| parent | e2d1c676b23a335b4fb8a528c99dfca2b82a1a39 (diff) | |
Separate vernac controls and regular commands.
Virtually all classifications of vernacular commands (the STM
classifier, "filtered commands", "navigation commands", etc.) were
broken in presence of control vernaculars like Time, Timeout, Fail.
Funny examples of bugs include Time Abort All in coqtop or Time Set Ltac
Debug in CoqIDE.
This change introduces a type separation between vernacular controls and
vernacular commands, together with an "under_control" combinator.
Diffstat (limited to 'toplevel/vernac.ml')
| -rw-r--r-- | toplevel/vernac.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 8fdaedbaf..24d414c88 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -111,13 +111,14 @@ let pr_open_cur_subgoals () = (* | _ -> false *) let rec interp_vernac ~check ~interactive doc sid (loc,com) = - let interp = function + let interp v = + match under_control v with | VernacLoad (verbosely, fname) -> - let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in + let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in let fname = CUnix.make_suffix fname ".v" in let f = Loadpath.locate_file fname in load_vernac ~verbosely ~check ~interactive doc sid f - | v -> + | _ -> (* XXX: We need to run this before add as the classification is highly dynamic and depends on the structure of the |