diff options
| -rw-r--r-- | ide/coq.ml | 9 | ||||
| -rw-r--r-- | ide/coq.mli | 1 | ||||
| -rw-r--r-- | ide/coq_commands.ml | 19 | ||||
| -rw-r--r-- | ide/coqide.ml | 3 |
4 files changed, 16 insertions, 16 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index e960170354..7b62ef1660 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -392,3 +392,12 @@ let make_cases s = tarr [] | _ -> raise Not_found + +let is_state_preserving = function + | VernacPrint _ | VernacPrintOption _ | VernacGlobalCheck _ + | VernacCheckMayEval _ | VernacSearch _ | VernacLocate _ + | VernacShow _ | VernacMemOption _ | VernacComments _ + | VernacChdir None | VernacNop -> + prerr_endline "state preserving command found"; true + | _ -> + false diff --git a/ide/coq.mli b/ide/coq.mli index 3acc686834..8625e93eeb 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -20,6 +20,7 @@ val interp : string -> Util.loc * Vernacexpr.vernac_expr val interp_last : Util.loc * Vernacexpr.vernac_expr -> unit val is_tactic : Vernacexpr.vernac_expr -> bool +val is_state_preserving : Vernacexpr.vernac_expr -> bool (* type hyp = (identifier * constr option * constr) * string *) diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml index 9598ee2f65..d51521ff71 100644 --- a/ide/coq_commands.ml +++ b/ide/coq_commands.ml @@ -194,14 +194,11 @@ let commands = [ let state_preserving = [ "Check"; "Eval"; - "Extract Constant"; - "Extract Inductive"; "Extraction"; - "Extraction Inline"; - "Extraction Language"; + "Extraction Library"; "Extraction Module"; - "Extraction NoInline"; "Inspect"; + "Locate"; "Print"; "Print All"; "Print Classes"; @@ -225,18 +222,13 @@ let state_preserving = [ "Pwd"; "Recursive Extraction"; - "Recursive Extraction Module"; + "Recursive Extraction Library"; "Search"; "SearchAbout"; "SearchPattern"; "SearchRewrite"; - "Set Printing Coercion"; - "Set Printing Coercions"; - "Set Printing Synth"; - "Set Printing Wildcard"; - "Show"; "Show Conjectures"; "Show Implicits"; @@ -252,9 +244,4 @@ let state_preserving = [ "Test Printing Wildcard"; "Recursive Extraction"; - - "Unset Printing Coercion"; - "Unset Printing Coercions"; - "Unset Printing Synth"; - "Unset Printing Wildcard"; ] diff --git a/ide/coqide.ml b/ide/coqide.ml index ae7dfbec57..26bb80b05f 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1236,6 +1236,9 @@ Please restart and report NOW."; raise e end); update_input () + | { ast = (_, a) } when is_state_preserving a -> + ignore (pop ()); + update_input () | _ -> self#backtrack_to_no_lock start end; |