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 | |
| 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')
| -rw-r--r-- | toplevel/vernac.ml | 7 | ||||
| -rw-r--r-- | toplevel/vernac.mli | 2 |
2 files changed, 5 insertions, 4 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 diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index f9a430026..8a798a98e 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -12,7 +12,7 @@ expected to handle and print errors in form of exceptions, however care is taken so the state machine is left in a consistent state. *) -val process_expr : Stm.doc -> Stateid.t -> Vernacexpr.vernac_expr Loc.located -> Stm.doc * Stateid.t +val process_expr : Stm.doc -> Stateid.t -> Vernacexpr.vernac_control Loc.located -> Stm.doc * Stateid.t (** [load_vernac echo sid file] Loads [file] on top of [sid], will echo the commands if [echo] is set. Callers are expected to handle |