diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
commit | 9043add656177eeac1491a73d2f3ab92bec0013c (patch) | |
tree | 2b0092c84bfbf718eca10c81f60b2640dc8cab05 /vernac/vernacprop.ml | |
parent | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (diff) |
Imported Upstream version 8.8.2upstream/8.8.2
Diffstat (limited to 'vernac/vernacprop.ml')
-rw-r--r-- | vernac/vernacprop.ml | 60 |
1 files changed, 60 insertions, 0 deletions
diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml new file mode 100644 index 00000000..a837b77a --- /dev/null +++ b/vernac/vernacprop.ml @@ -0,0 +1,60 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* We define some high-level properties of vernacular commands, used + mainly by the UI components *) + +open Vernacexpr + +let rec under_control = function + | VernacExpr (_, c) -> c + | VernacRedirect (_,{CAst.v=c}) + | VernacTime (_,{CAst.v=c}) + | VernacFail c + | VernacTimeout (_,c) -> under_control c + +let rec has_Fail = function + | VernacExpr _ -> false + | VernacRedirect (_,{CAst.v=c}) + | VernacTime (_,{CAst.v=c}) + | VernacTimeout (_,c) -> has_Fail c + | VernacFail _ -> true + +(* Navigation commands are allowed in a coqtop session but not in a .v file *) +let is_navigation_vernac_expr = function + | VernacResetInitial + | VernacResetName _ + | VernacBacktrack _ + | VernacBackTo _ + | VernacBack _ -> true + | _ -> false + +let is_navigation_vernac c = + is_navigation_vernac_expr (under_control c) + +let rec is_deep_navigation_vernac = function + | VernacTime (_,{CAst.v=c}) -> is_deep_navigation_vernac c + | VernacRedirect (_, {CAst.v=c}) + | VernacTimeout (_,c) | VernacFail c -> is_navigation_vernac c + | VernacExpr _ -> false + +(* NB: Reset is now allowed again as asked by A. Chlipala *) +let is_reset = function + | VernacExpr ( _, VernacResetInitial) + | VernacExpr (_, VernacResetName _) -> true + | _ -> false + +let is_debug cmd = match under_control cmd with + | VernacSetOption (_, ["Ltac";"Debug"], _) -> true + | _ -> false + +let is_undo cmd = match under_control cmd with + | VernacUndo _ | VernacUndoTo _ -> true + | _ -> false |