diff options
Diffstat (limited to 'vernac/vernacprop.ml')
-rw-r--r-- | vernac/vernacprop.ml | 39 |
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 |