1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* 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 (_,(_,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 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 (_,c) -> is_deep_navigation_vernac c
| VernacRedirect (_, (_,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_query cmd = match under_control cmd with
| VernacChdir None
| VernacMemOption _
| VernacPrintOption _
| VernacCheckMayEval _
| VernacGlobalCheck _
| VernacPrint _
| VernacSearch _
| VernacLocate _ -> true
| _ -> false
let is_undo cmd = match under_control cmd with
| VernacUndo _ | VernacUndoTo _ -> true
| _ -> false
|
