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 /intf | |
| 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 'intf')
| -rw-r--r-- | intf/vernacexpr.ml | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index c7a9db1cb..a90e5501a 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -315,13 +315,8 @@ type cumulative_inductive_parsing_flag = (** {6 The type of vernacular expressions} *) type vernac_expr = - (* Control *) - | VernacLoad of verbose_flag * string - | VernacTime of vernac_expr located - | VernacRedirect of string * vernac_expr located - | VernacTimeout of int * vernac_expr - | VernacFail of vernac_expr + | VernacLoad of verbose_flag * string (* Syntax *) | VernacSyntaxExtension of bool * (lstring * syntax_modifier list) | VernacOpenCloseScope of bool * scope_name @@ -482,6 +477,14 @@ and vernac_argument_status = { implicit_status : vernac_implicit_status; } +type vernac_control = + | VernacExpr of vernac_expr + (* Control *) + | VernacTime of vernac_control located + | VernacRedirect of string * vernac_control located + | VernacTimeout of int * vernac_control + | VernacFail of vernac_control + (* A vernac classifier provides information about the exectuion of a command: |