Merge PR#441: Port Toplevel to the Stm API

5 files changed, 77 insertions, 68 deletions

diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index 283c095eb..d631fae8a 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -1,3 +1,4 @@
+Vernacprop
 Lemmas
 Himsg
 ExplainErr
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 53d49ddbc..287584d56 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -84,24 +84,10 @@ let show_universes () =
     Feedback.msg_notice (Termops.pr_evar_universe_context (Evd.evar_universe_context sigma));
     Feedback.msg_notice (str"Normalized constraints: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) ctx)
 
-let show_prooftree () =
-  (* Spiwack: proof tree is currently not working *)
-  ()
-
-let enable_goal_printing = ref true
-
-let print_subgoals () =
-  if !enable_goal_printing && is_verbose ()
-  then begin
-    Feedback.msg_notice (pr_open_subgoals ())
-  end
-
-let try_print_subgoals () =
-  try print_subgoals () with Proof_global.NoCurrentProof | UserError _ -> ()
-
-
-  (* Simulate the Intro(s) tactic *)
+(* Spiwack: proof tree is currently not working *)
+let show_prooftree () = ()
 
+(* Simulate the Intro(s) tactic *)
 let show_intro all =
   let open EConstr in
   let pf = get_pftreestate() in
@@ -513,8 +499,6 @@ let vernac_start_proof locality p kind l lettop =
 	(str "Let declarations can only be used in proof editing mode.");
   start_proof_and_print (local, p, Proof kind) l no_hook
 
-let qed_display_script = ref true
-
 let vernac_end_proof ?proof = function
   | Admitted          -> save_proof ?proof Admitted
   | Proved (_,_) as e -> save_proof ?proof e
@@ -1381,15 +1365,6 @@ let _ =
   declare_bool_option
     { optsync  = true;
       optdepr  = false;
-      optname  = "record printing";
-      optkey   = ["Printing";"Records"];
-      optread  = (fun () -> !Flags.record_print);
-      optwrite = (fun b -> Flags.record_print := b) }
-
-let _ =
-  declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
       optname  = "use of the program extension";
       optkey   = ["Program";"Mode"];
       optread  = (fun () -> !Flags.program_mode);
@@ -1438,15 +1413,6 @@ let _ =
 
 let _ =
   declare_int_option
-    { optsync  = false;
-      optdepr  = false;
-      optname  = "the hypotheses limit";
-      optkey   = ["Hyps";"Limit"];
-      optread  = Flags.print_hyps_limit;
-      optwrite = Flags.set_print_hyps_limit }
-
-let _ =
-  declare_int_option
     { optsync  = true;
       optdepr  = false;
       optname  = "the printing depth";
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 7cdc8dd06..fb2899515 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -11,42 +11,15 @@ open Misctypes
 val dump_global : Libnames.reference or_by_notation -> unit
 
 (** Vernacular entries *)
-
-val show_prooftree : unit -> unit
-
-val show_node : unit -> unit
-
 val vernac_require :
   Libnames.reference option -> bool option -> Libnames.reference list -> unit
 
-(** This function can be used by any command that want to observe terms
-   in the context of the current goal *)
-val get_current_context_of_args : int option -> Evd.evar_map * Environ.env
-
 (** The main interpretation function of vernacular expressions *)
-val interp : 
+val interp :
   ?verbosely:bool ->
   ?proof:Proof_global.closed_proof ->
     Loc.t * Vernacexpr.vernac_expr -> unit
 
-(** Print subgoals when the verbose flag is on.
-    Meant to be used inside vernac commands from plugins. *)
-
-val print_subgoals : unit -> unit
-val try_print_subgoals : unit -> unit
-
-(** The printing of goals via [print_subgoals] or during
-    [interp] can be controlled by the following flag.
-    Used for instance by coqide, since it has its own
-    goal-fetching mechanism. *)
-
-val enable_goal_printing : bool ref
-
-(** Should Qed try to display the proof script ?
-    True by default, but false in ProofGeneral and coqIDE *)
-
-val qed_display_script : bool ref
-
 (** Prepare a "match" template for a given inductive type.
     For each branch of the match, we list the constructor name
     followed by enough pattern variables.
@@ -55,9 +28,6 @@ val qed_display_script : bool ref
 
 val make_cases : string -> string list list
 
-val vernac_end_proof :
-  ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> unit
-
 val with_fail : bool -> (unit -> unit) -> unit
 
 val command_focus : unit Proof.focus_kind
diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml
new file mode 100644
index 000000000..ec78d6012
--- /dev/null
+++ b/vernac/vernacprop.ml
@@ -0,0 +1,53 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \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
+
+(* Navigation commands are allowed in a coqtop session but not in a .v file *)
+let rec is_navigation_vernac = function
+  | VernacResetInitial
+  | VernacResetName _
+  | VernacBacktrack _
+  | VernacBackTo _
+  | VernacBack _
+  | VernacStm _ -> true
+  | VernacRedirect (_, (_,c))
+  | VernacTime (_,c) ->
+      is_navigation_vernac c (* Time Back* is harmless *)
+  | c -> is_deep_navigation_vernac c
+
+and is_deep_navigation_vernac = function
+  | VernacTimeout (_,c) | VernacFail c -> is_navigation_vernac c
+  | _ -> false
+
+(* NB: Reset is now allowed again as asked by A. Chlipala *)
+let is_reset = function
+  | VernacResetInitial | VernacResetName _ -> true
+  | _ -> false
+
+let is_debug cmd = match cmd with
+  | VernacSetOption (["Ltac";"Debug"], _) -> true
+  | _ -> false
+
+let is_query cmd = match cmd with
+  | VernacChdir None
+  | VernacMemOption _
+  | VernacPrintOption _
+  | VernacCheckMayEval _
+  | VernacGlobalCheck _
+  | VernacPrint _
+  | VernacSearch _
+  | VernacLocate _ -> true
+  | _ -> false
+
+let is_undo cmd = match cmd with
+  | VernacUndo _ | VernacUndoTo _ -> true
+  | _ -> false
diff --git a/vernac/vernacprop.mli b/vernac/vernacprop.mli
new file mode 100644
index 000000000..c235ecfb5
--- /dev/null
+++ b/vernac/vernacprop.mli
@@ -0,0 +1,19 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \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
+
+val is_navigation_vernac : vernac_expr -> bool
+val is_deep_navigation_vernac : vernac_expr -> bool
+val is_reset : vernac_expr -> bool
+val is_query : vernac_expr -> bool
+val is_debug : vernac_expr -> bool
+val is_undo : vernac_expr -> bool