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.

3 files changed, 14 insertions, 13 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 444f36833b..c18c6810f7 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
 
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index b766f0c6bb..c934d38a25 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -503,8 +503,7 @@ module Vernac_ =
     let gallina_ext = gec_vernac "gallina_ext"
     let command = gec_vernac "command"
     let syntax = gec_vernac "syntax_command"
-    let vernac = gec_vernac "Vernac.vernac"
-    let vernac_eoi = eoi_entry vernac
+    let vernac_control = gec_vernac "Vernac.vernac_control"
     let rec_definition = gec_vernac "Vernac.rec_definition"
     let red_expr = make_gen_entry utactic "red_expr"
     let hint_info = gec_vernac "hint_info"
@@ -517,7 +516,7 @@ module Vernac_ =
       let act_eoi = Gram.action (fun _ loc -> None) in
       let rule = [
         ([ Symbols.stoken Tok.EOI ], act_eoi);
-        ([ Symbols.snterm (Gram.Entry.obj vernac) ], act_vernac );
+        ([ Symbols.snterm (Gram.Entry.obj vernac_control) ], act_vernac );
       ] in
       uncurry (Gram.extend main_entry) (None, make_rule rule)
 
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 3ca013a968..756d9487df 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -251,9 +251,8 @@ module Vernac_ :
     val gallina_ext : vernac_expr Gram.entry
     val command : vernac_expr Gram.entry
     val syntax : vernac_expr Gram.entry
-    val vernac : vernac_expr Gram.entry
+    val vernac_control : vernac_control Gram.entry
     val rec_definition : (fixpoint_expr * decl_notation list) Gram.entry
-    val vernac_eoi : vernac_expr Gram.entry
     val noedit_mode : vernac_expr Gram.entry
     val command_entry : vernac_expr Gram.entry
     val red_expr : raw_red_expr Gram.entry
@@ -261,7 +260,7 @@ module Vernac_ :
   end
 
 (** The main entry: reads an optional vernac command *)
-val main_entry : (Loc.t * vernac_expr) option Gram.entry
+val main_entry : (Loc.t * vernac_control) option Gram.entry
 
 (** Handling of the proof mode entry *)
 val get_command_entry : unit -> vernac_expr Gram.entry