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 /parsing/g_vernac.ml4 | |
| 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 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 17 |
1 files changed, 10 insertions, 7 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 444f36833..c18c6810f 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -65,14 +65,17 @@ let parse_compat_version ?(allow_old = true) = let open Flags in function Pp.(str "Unknown compatibility version \"" ++ str s ++ str "\".") GEXTEND Gram - GLOBAL: vernac gallina_ext noedit_mode subprf; - vernac: FIRST + GLOBAL: vernac_control gallina_ext noedit_mode subprf; + vernac_control: FIRST [ [ IDENT "Time"; c = located_vernac -> VernacTime c | IDENT "Redirect"; s = ne_string; c = located_vernac -> VernacRedirect (s, c) - | IDENT "Timeout"; n = natural; v = vernac -> VernacTimeout(n,v) - | IDENT "Fail"; v = vernac -> VernacFail v - - | IDENT "Local"; v = vernac_poly -> VernacLocal (true, v) + | IDENT "Timeout"; n = natural; v = vernac_control -> VernacTimeout(n,v) + | IDENT "Fail"; v = vernac_control -> VernacFail v + | v = vernac -> VernacExpr(v) ] + ] + ; + vernac: + [ [ IDENT "Local"; v = vernac_poly -> VernacLocal (true, v) | IDENT "Global"; v = vernac_poly -> VernacLocal (false, v) | v = vernac_poly -> v ] @@ -111,7 +114,7 @@ GEXTEND Gram ; located_vernac: - [ [ v = vernac -> Loc.tag ~loc:!@loc v ] ] + [ [ v = vernac_control -> Loc.tag ~loc:!@loc v ] ] ; END |