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.

1 files changed, 28 insertions, 11 deletions

diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml
index 3cff1f14c..4a01ef2ef 100644
--- a/vernac/vernacprop.ml
+++ b/vernac/vernacprop.ml
@@ -11,32 +11,49 @@
 
 open Vernacexpr
 
+let rec under_control = function
+  | VernacExpr c -> c
+  | VernacRedirect (_,(_,c))
+  | VernacTime (_,c)
+  | VernacFail c
+  | VernacTimeout (_,c) -> under_control c
+
+let rec has_Fail = function
+  | VernacExpr c -> false
+  | VernacRedirect (_,(_,c))
+  | VernacTime (_,c)
+  | VernacTimeout (_,c) -> has_Fail c
+  | VernacFail _ -> true
+
 (* Navigation commands are allowed in a coqtop session but not in a .v file *)
-let rec is_navigation_vernac = function
+let is_navigation_vernac_expr = function
   | VernacResetInitial
   | VernacResetName _
   | VernacBacktrack _
   | VernacBackTo _
   | VernacBack _ -> true
-  | VernacRedirect (_, (_,c))
-  | VernacTime (_,c) ->
-      is_navigation_vernac c (* Time Back* is harmless *)
-  | c -> is_deep_navigation_vernac c
+  | _ -> false
 
-and is_deep_navigation_vernac = function
+let is_navigation_vernac c =
+  is_navigation_vernac_expr (under_control c)
+
+let rec is_deep_navigation_vernac = function
+  | VernacTime (_,c) -> is_deep_navigation_vernac c
+  | VernacRedirect (_, (_,c))
   | VernacTimeout (_,c) | VernacFail c -> is_navigation_vernac c
-  | _ -> false
+  | VernacExpr _ -> false
 
 (* NB: Reset is now allowed again as asked by A. Chlipala *)
 let is_reset = function
-  | VernacResetInitial | VernacResetName _ -> true
+  | VernacExpr VernacResetInitial
+  | VernacExpr (VernacResetName _) -> true
   | _ -> false
 
-let is_debug cmd = match cmd with
+let is_debug cmd = match under_control cmd with
   | VernacSetOption (["Ltac";"Debug"], _) -> true
   | _ -> false
 
-let is_query cmd = match cmd with
+let is_query cmd = match under_control cmd with
   | VernacChdir None
   | VernacMemOption _
   | VernacPrintOption _
@@ -47,6 +64,6 @@ let is_query cmd = match cmd with
   | VernacLocate _ -> true
   | _ -> false
 
-let is_undo cmd = match cmd with
+let is_undo cmd = match under_control cmd with
   | VernacUndo _ | VernacUndoTo _ -> true
   | _ -> false