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.

2 files changed, 32 insertions, 28 deletions

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 46ef2ac03..418d4a0b8 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -535,16 +535,25 @@ open Decl_kinds
       | SsFwdClose e -> "("^aux e^")*"
     in Pp.str (aux e)
 
-  let rec pr_vernac_body v =
+  let rec pr_vernac_expr v =
     let return = tag_vernac v in
     match v with
       | VernacPolymorphic (poly, v) ->
         let s = if poly then keyword "Polymorphic" else keyword "Monomorphic" in
-        return (s ++ spc () ++ pr_vernac_body v)
+        return (s ++ spc () ++ pr_vernac_expr v)
       | VernacProgram v ->
-        return (keyword "Program" ++ spc() ++ pr_vernac_body v)
+        return (keyword "Program" ++ spc() ++ pr_vernac_expr v)
       | VernacLocal (local, v) ->
-        return (pr_locality local ++ spc() ++ pr_vernac_body v)
+        return (pr_locality local ++ spc() ++ pr_vernac_expr v)
+
+      | VernacLoad (f,s) ->
+        return (
+          keyword "Load"
+          ++ if f then
+              (spc() ++ keyword "Verbose" ++ spc())
+            else
+              spc() ++ qs s
+        )
 
       (* Proof management *)
       | VernacAbortAll ->
@@ -607,24 +616,6 @@ open Decl_kinds
       | VernacRestoreState s ->
         return  (keyword "Restore State" ++ spc() ++ qs s)
 
-    (* Control *)
-      | VernacLoad (f,s) ->
-        return (
-          keyword "Load"
-          ++ if f then
-              (spc() ++ keyword "Verbose" ++ spc())
-            else
-              spc() ++ qs s
-        )
-      | VernacTime (_,v) ->
-        return (keyword "Time" ++ spc() ++ pr_vernac_body v)
-      | VernacRedirect (s, (_,v)) ->
-        return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_body v)
-      | VernacTimeout(n,v) ->
-        return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac_body v)
-      | VernacFail v ->
-        return (keyword "Fail" ++ spc() ++ pr_vernac_body v)
-
     (* Syntax *)
       | VernacOpenCloseScope (opening,sc) ->
         return (
@@ -1228,6 +1219,19 @@ open Decl_kinds
     with Not_found ->
       hov 1 (str "TODO(" ++ str (fst s) ++ spc () ++ prlist_with_sep sep pr_arg cl ++ str ")")
 
-  let pr_vernac v =
-    try pr_vernac_body v ++ sep_end v
-    with e -> CErrors.print e
+  let rec pr_vernac_control v =
+    let return = tag_vernac v in
+    match v with
+    | VernacExpr v' -> pr_vernac_expr v' ++ sep_end v'
+    | VernacTime (_,v) ->
+      return (keyword "Time" ++ spc() ++ pr_vernac_control v)
+    | VernacRedirect (s, (_,v)) ->
+      return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_control v)
+    | VernacTimeout(n,v) ->
+      return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac_control v)
+    | VernacFail v ->
+      return (keyword "Fail" ++ spc() ++ pr_vernac_control v)
+
+    let pr_vernac v =
+      try pr_vernac_control v
+      with e -> CErrors.print e
diff --git a/printing/ppvernac.mli b/printing/ppvernac.mli
index cf27b413c..34b4fb97f 100644
--- a/printing/ppvernac.mli
+++ b/printing/ppvernac.mli
@@ -12,11 +12,11 @@
 (** Prints a fixpoint body *)
 val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.t
 
-(** Prints a vernac expression *)
-val pr_vernac_body : Vernacexpr.vernac_expr -> Pp.t
+(** Prints a vernac expression without dot *)
+val pr_vernac_expr : Vernacexpr.vernac_expr -> Pp.t
 
 (** Prints a "proof using X" clause. *)
 val pr_using : Vernacexpr.section_subset_expr -> Pp.t
 
 (** Prints a vernac expression and closes it with a dot. *)
-val pr_vernac : Vernacexpr.vernac_expr -> Pp.t
+val pr_vernac : Vernacexpr.vernac_control -> Pp.t