aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-04-12 18:35:21 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-04-12 18:35:21 +0200
commita5c150a6a7fa980c5850aa247e62d02e29773235 (patch)
treee8f9a6211c3626d80d8427887bf181d10a3476f9
parenta74d64efb554e9fd57b8ec97fca7677033cc4fc4 (diff)
parentb63b9a86b09856262b5b7bb2b3bb01f704032d41 (diff)
Merge PR#441: Port Toplevel to the Stm API
Diffstat
-rw-r--r--dev/doc/changes.txt30
-rw-r--r--ide/coqOps.ml12
-rw-r--r--ide/ide_slave.ml75
-rw-r--r--ide/interface.mli6
-rw-r--r--ide/xmlprotocol.ml10
-rw-r--r--interp/constrextern.ml16
-rw-r--r--kernel/term_typing.ml2
-rw-r--r--lib/feedback.ml10
-rw-r--r--lib/feedback.mli23
-rw-r--r--lib/flags.ml9
-rw-r--r--lib/flags.mli26
-rw-r--r--plugins/ltac/profile_ltac.ml2
-rw-r--r--printing/printer.ml17
-rw-r--r--stm/asyncTaskQueue.ml2
-rw-r--r--stm/stm.ml385
-rw-r--r--stm/stm.mli57
-rw-r--r--toplevel/coqinit.ml11
-rw-r--r--toplevel/coqinit.mli2
-rw-r--r--toplevel/coqloop.ml59
-rw-r--r--toplevel/coqloop.mli2
-rw-r--r--toplevel/coqtop.ml39
-rw-r--r--toplevel/vernac.ml182
-rw-r--r--toplevel/vernac.mli26
-rw-r--r--vernac/vernac.mllib1
-rw-r--r--vernac/vernacentries.ml40
-rw-r--r--vernac/vernacentries.mli32
-rw-r--r--vernac/vernacprop.ml53
-rw-r--r--vernac/vernacprop.mli19
28 files changed, 540 insertions, 608 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 2080f164a..7f915b781 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -146,6 +146,36 @@ document type". This allows for a more uniform handling of printing
module Tag
+** Stm API **
+
+- We have streamlined the `Stm` API, now `add` and `query` take a
+ `coq_parsable` instead a `string` so clients can have more control
+ over their input stream. As a consequence, their types have been
+ modified.
+
+- The main parsing entry point has also been moved to the
+ `Stm`. Parsing is considered a synchronous operation so it will
+ either succeed or raise an exception.
+
+- `Feedback` is now only emitted for asynchronous operations. As a
+ consequence, it always carries a valid stateid and the type has
+ changed to accommodate that.
+
+- A few unused hooks were removed due to cleanups, no clients known.
+
+** Toplevel and Vernacular API **
+
+- The components related to vernacular interpretation have been moved
+ to their own folder `vernac/` whereas toplevel now contains the
+ proper toplevel shell and compiler.
+
+- Coq's toplevel has been ported to directly use the common `Stm`
+ API. The signature of a few functions has changed as a result.
+
+** XML Protocol **
+
+- The legacy `Interp` call has been turned into a noop.
+
=========================================
= CHANGES BETWEEN COQ V8.5 AND COQ V8.6 =
=========================================
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 3d6a2583f..eb97755fa 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -414,11 +414,7 @@ object(self)
buffer#apply_tag Tags.Script.tooltip ~start ~stop;
add_tooltip sentence pre post markup
- method private is_dummy_id id =
- match id with
- | Edit 0 -> true
- | State id when Stateid.equal id Stateid.dummy -> true
- | _ -> false
+ method private is_dummy_id id = Stateid.equal id Stateid.dummy
method private enqueue_feedback msg =
(* Minilib.log ("Feedback received: " ^ Xml_printer.to_string_fmt (Xmlprotocol.of_feedback msg)); *)
@@ -433,8 +429,7 @@ object(self)
let sentence =
let finder _ state_id s =
match state_id, id with
- | Some id', State id when Stateid.equal id id' -> Some (state_id, s)
- | _, Edit id when id = s.edit_id -> Some (state_id, s)
+ | Some id', id when Stateid.equal id id' -> Some (state_id, s)
| _ -> None in
try Some (Doc.find_map document finder)
with Not_found -> None in
@@ -503,8 +498,7 @@ object(self)
else
try
match id, Doc.tip document with
- | Edit _, _ -> ()
- | State id1, id2 when Stateid.newer_than id2 id1 -> ()
+ | id1, id2 when Stateid.newer_than id2 id1 -> ()
| _ -> Queue.add msg feedbacks
with Doc.Empty | Invalid_argument _ -> Queue.add msg feedbacks
end;
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 0dfa03cca..4b95e983d 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -8,6 +8,7 @@
(************************************************************************)
open Vernacexpr
+open Vernacprop
open CErrors
open Util
open Pp
@@ -60,25 +61,6 @@ let is_known_option cmd = match cmd with
| VernacUnsetOption o -> coqide_known_option o
| _ -> 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
-
(** Check whether a command is forbidden in the IDE *)
let ide_cmd_checks (loc,ast) =
@@ -86,16 +68,19 @@ let ide_cmd_checks (loc,ast) =
if is_debug ast then
user_error "Debug mode not available in the IDE";
if is_known_option ast then
- Feedback.msg_warning (strbrk "Set this option from the IDE menu instead");
- if Vernac.is_navigation_vernac ast || is_undo ast then
- Feedback.msg_warning (strbrk "Use IDE navigation instead");
+ Feedback.msg_warning ~loc (strbrk "Set this option from the IDE menu instead");
+ if is_navigation_vernac ast || is_undo ast then
+ Feedback.msg_warning ~loc (strbrk "Use IDE navigation instead");
if is_query ast then
- Feedback.msg_warning (strbrk "Query commands should not be inserted in scripts")
+ Feedback.msg_warning ~loc (strbrk "Query commands should not be inserted in scripts")
(** Interpretation (cf. [Ide_intf.interp]) *)
let add ((s,eid),(sid,verbose)) =
- let newid, rc = Stm.add ~ontop:sid verbose ~check:ide_cmd_checks eid s in
+ let pa = Pcoq.Gram.parsable (Stream.of_string s) in
+ let loc_ast = Stm.parse_sentence sid pa in
+ ide_cmd_checks loc_ast;
+ let newid, rc = Stm.add ~ontop:sid verbose loc_ast in
let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in
(* TODO: the "" parameter is a leftover of the times the protocol
* used to include stderr/stdout output.
@@ -122,12 +107,14 @@ let edit_at id =
* as not to break the core protocol for this minor change, but it should
* be removed in the next version of the protocol.
*)
-let query (s,id) = Stm.query ~at:id s; ""
+let query (s,id) =
+ let pa = Pcoq.Gram.parsable (Stream.of_string s) in
+ Stm.query ~at:id pa; ""
let annotate phrase =
let (loc, ast) =
let pa = Pcoq.Gram.parsable (Stream.of_string phrase) in
- Vernac.parse_sentence (pa,None)
+ Stm.parse_sentence (Stm.get_current_state ()) pa
in
(* XXX: Width should be a parameter of annotate... *)
Richpp.richpp_of_pp 78 (Ppvernac.pr_vernac ast)
@@ -370,43 +357,28 @@ let init =
fun file ->
if !initialized then anomaly (str "Already initialized")
else begin
+ let init_sid = Stm.get_current_state () in
initialized := true;
match file with
- | None -> Stm.get_current_state ()
+ | None -> init_sid
| Some file ->
let dir = Filename.dirname file in
let open Loadpath in let open CUnix in
let initial_id, _ =
- if not (is_in_load_paths (physical_path_of_string dir)) then
- Stm.add false ~ontop:(Stm.get_current_state ())
- 0 (Printf.sprintf "Add LoadPath \"%s\". " dir)
- else Stm.get_current_state (), `NewTip in
+ if not (is_in_load_paths (physical_path_of_string dir)) then begin
+ let pa = Pcoq.Gram.parsable (Stream.of_string (Printf.sprintf "Add LoadPath \"%s\". " dir)) in
+ let loc_ast = Stm.parse_sentence init_sid pa in
+ Stm.add false ~ontop:init_sid loc_ast
+ end else init_sid, `NewTip in
if Filename.check_suffix file ".v" then
Stm.set_compilation_hints file;
Stm.finish ();
initial_id
end
-(* Retrocompatibility stuff *)
+(* Retrocompatibility stuff, disabled since 8.7 *)
let interp ((_raw, verbose), s) =
- let vernac_parse s =
- let pa = Pcoq.Gram.parsable (Stream.of_string s) in
- Flags.with_option Flags.we_are_parsing (fun () ->
- match Pcoq.Gram.entry_parse Pcoq.main_entry pa with
- | None -> raise (Invalid_argument "vernac_parse")
- | Some ast -> ast)
- () in
- Stm.interp verbose (vernac_parse s);
- (* TODO: the "" parameter is a leftover of the times the protocol
- * used to include stderr/stdout output.
- *
- * Currently, we force all the output meant for the to go via the
- * feedback mechanism, and we don't manipulate stderr/stdout, which
- * are left to the client's discrection. The parameter is still there
- * as not to break the core protocol for this minor change, but it should
- * be removed in the next version of the protocol.
- *)
- Stm.get_current_state (), CSig.Inl ""
+ Stateid.dummy, CSig.Inr "The interp call has been disabled, please use Add."
(** When receiving the Quit call, we don't directly do an [exit 0],
but rather set this reference, in order to send a final answer
@@ -494,9 +466,6 @@ let loop () =
let xml_ic = Xml_parser.make (Xml_parser.SLexbuf in_lb) in
let () = Xml_parser.check_eof xml_ic false in
ignore (Feedback.add_feeder (slave_feeder (!msg_format ()) xml_oc));
- (* We'll handle goal fetching and display in our own way *)
- Vernacentries.enable_goal_printing := false;
- Vernacentries.qed_display_script := false;
while not !quit do
try
let xml_query = Xml_parser.parse xml_ic in
diff --git a/ide/interface.mli b/ide/interface.mli
index 9ed606258..62f63aefb 100644
--- a/ide/interface.mli
+++ b/ide/interface.mli
@@ -111,8 +111,10 @@ type coq_info = {
(** Calls result *)
type location = (int * int) option (* start and end of the error *)
-type state_id = Feedback.state_id
-type edit_id = Feedback.edit_id
+type state_id = Stateid.t
+
+(* Obsolete *)
+type edit_id = int
(* The fail case carries the current state_id of the prover, the GUI
should probably retract to that point *)
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
index d7950e5fd..bf52b0b52 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/xmlprotocol.ml
@@ -907,9 +907,7 @@ let of_feedback_content = function
of_string filename ]
| Message (l,loc,m) -> constructor "feedback_content" "message" [ of_message l loc m ]
-let of_edit_or_state_id = function
- | Edit id -> ["object","edit"], of_edit_id id
- | State id -> ["object","state"], of_stateid id
+let of_edit_or_state_id id = ["object","state"], of_stateid id
let of_feedback msg =
let content = of_feedback_content msg.contents in
@@ -921,12 +919,8 @@ let of_feedback msg_fmt =
msg_format := msg_fmt; of_feedback
let to_feedback xml = match xml with
- | Element ("feedback", ["object","edit";"route",route], [id;content]) -> {
- id = Edit(to_edit_id id);
- route = int_of_string route;
- contents = to_feedback_content content }
| Element ("feedback", ["object","state";"route",route], [id;content]) -> {
- id = State(to_stateid id);
+ id = to_stateid id;
route = int_of_string route;
contents = to_feedback_content content }
| x -> raise (Marshal_error("feedback",x))
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index f272d219a..59b8b4e5b 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -85,6 +85,20 @@ let without_specific_symbols l f =
(**********************************************************************)
(* Control printing of records *)
+(* Set Record Printing flag *)
+let record_print = ref true
+
+let _ =
+ let open Goptions in
+ declare_bool_option
+ { optsync = true;
+ optdepr = false;
+ optname = "record printing";
+ optkey = ["Printing";"Records"];
+ optread = (fun () -> !record_print);
+ optwrite = (fun b -> record_print := b) }
+
+
let is_record indsp =
try
let _ = Recordops.lookup_structure indsp in
@@ -658,7 +672,7 @@ let rec extern inctx scopes vars r =
()
else if PrintingConstructor.active (fst cstrsp) then
raise Exit
- else if not !Flags.record_print then
+ else if not !record_print then
raise Exit;
let projs = struc.Recordops.s_PROJ in
let locals = struc.Recordops.s_PROJKIND in
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index f43b01d1b..eeb9c421a 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -223,7 +223,7 @@ let rec unzip ctx j =
let feedback_completion_typecheck =
let open Feedback in
Option.iter (fun state_id ->
- feedback ~id:(State state_id) Feedback.Complete)
+ feedback ~id:state_id Feedback.Complete)
let infer_declaration ~trust env kn dcl =
match dcl with
diff --git a/lib/feedback.ml b/lib/feedback.ml
index 7d9d6bf7f..df6fe3a62 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -15,9 +15,6 @@ type level =
| Warning
| Error
-type edit_id = int
-type state_id = Stateid.t
-type edit_or_state_id = Edit of edit_id | State of state_id
type route_id = int
type feedback_content =
@@ -38,9 +35,9 @@ type feedback_content =
| Message of level * Loc.t option * Pp.std_ppcmds
type feedback = {
- id : edit_or_state_id;
+ id : Stateid.t;
+ route : route_id;
contents : feedback_content;
- route : route_id;
}
let default_route = 0
@@ -56,7 +53,8 @@ let add_feeder =
let del_feeder fid = Hashtbl.remove feeders fid
-let feedback_id = ref (Edit 0)
+let default_route = 0
+let feedback_id = ref Stateid.dummy
let feedback_route = ref default_route
let set_id_for_feedback ?(route=default_route) i =
diff --git a/lib/feedback.mli b/lib/feedback.mli
index 4bbdfcb5b..bdd236ac7 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -16,11 +16,8 @@ type level =
| Warning
| Error
-(** Coq "semantic" infos obtained during parsing/execution *)
-type edit_id = int
-type state_id = Stateid.t
-type edit_or_state_id = Edit of edit_id | State of state_id
+(** Coq "semantic" infos obtained during execution *)
type route_id = int
val default_route : route_id
@@ -46,17 +43,16 @@ type feedback_content =
| Message of level * Loc.t option * Pp.std_ppcmds
type feedback = {
- id : edit_or_state_id; (* The document part concerned *)
- contents : feedback_content; (* The payload *)
+ id : Stateid.t; (* The document part concerned *)
route : route_id; (* Extra routing info *)
+ contents : feedback_content; (* The payload *)
}
(** {6 Feedback sent, even asynchronously, to the user interface} *)
-(* Morally the parser gets a string and an edit_id, and gives back an AST.
- * Feedbacks during the parsing phase are attached to this edit_id.
- * The interpreter assignes an exec_id to the ast, and feedbacks happening
- * during interpretation are attached to the exec_id.
- * Only one among state_id and edit_id can be provided. *)
+
+(* The interpreter assignes an state_id to the ast, and feedbacks happening
+ * during interpretation are attached to it.
+ *)
(** [add_feeder f] adds a feeder listiner [f], returning its id *)
val add_feeder : (feedback -> unit) -> int
@@ -67,11 +63,10 @@ val del_feeder : int -> unit
(** [feedback ?id ?route fb] produces feedback fb, with [route] and
[id] set appropiatedly, if absent, it will use the defaults set by
[set_id_for_feedback] *)
-val feedback :
- ?id:edit_or_state_id -> ?route:route_id -> feedback_content -> unit
+val feedback : ?id:Stateid.t -> ?route:route_id -> feedback_content -> unit
(** [set_id_for_feedback route id] Set the defaults for feedback *)
-val set_id_for_feedback : ?route:route_id -> edit_or_state_id -> unit
+val set_id_for_feedback : ?route:route_id -> Stateid.t -> unit
(** {6 output functions}
diff --git a/lib/flags.ml b/lib/flags.ml
index 5b080151c..d87d9e729 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -86,8 +86,6 @@ let in_toplevel = ref false
let profile = false
let print_emacs = ref false
-let coqtop_ui = ref false
-
let xml_export = ref false
let ide_slave = ref false
@@ -97,7 +95,6 @@ let time = ref false
let raw_print = ref false
-let record_print = ref true
let univ_print = ref false
@@ -183,12 +180,6 @@ let warn = ref true
let make_warn flag = warn := flag; ()
let if_warn f x = if !warn then f x
-(* The number of printed hypothesis in a goal *)
-
-let print_hyps_limit = ref (None : int option)
-let set_print_hyps_limit n = print_hyps_limit := n
-let print_hyps_limit () = !print_hyps_limit
-
(* Flags for external tools *)
let browser_cmd_fmt =
diff --git a/lib/flags.mli b/lib/flags.mli
index bd365e653..c5c4a15aa 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -8,6 +8,8 @@
(** Global options of the system. *)
+(** Command-line flags *)
+
val boot : bool ref
val load_init : bool ref
@@ -16,8 +18,11 @@ type compilation_mode = BuildVo | BuildVio | Vio2Vo
val compilation_mode : compilation_mode ref
val compilation_output_name : string option ref
+(* Flag set when the test-suite is called. Its only effect to display
+ verbose information for `Fail` *)
val test_mode : bool ref
+(** Async-related flags *)
type async_proofs = APoff | APonLazy | APon
val async_proofs_mode : async_proofs ref
type cache = Force
@@ -46,20 +51,27 @@ val in_toplevel : bool ref
val profile : bool
-val print_emacs : bool ref
-val coqtop_ui : bool ref
+(* Legacy flags *)
+(* -emacs option: printing includes emacs tags, will affect stm caching. *)
+val print_emacs : bool ref
+(* -xml option: xml hooks will be called *)
val xml_export : bool ref
+(* -ide_slave: printing will be more verbose, will affect stm caching *)
val ide_slave : bool ref
val ideslave_coqtop_flags : string option ref
+(* -time option: every command will be wrapped with `Time` *)
val time : bool ref
+(* development flag to detect race conditions, it should go away. *)
val we_are_parsing : bool ref
+(* Set Printing All flag. For some reason it is a global flag *)
val raw_print : bool ref
-val record_print : bool ref
+
+(* Univ print flag, never set anywere. Maybe should belong to Univ? *)
val univ_print : bool ref
type compat_version = V8_2 | V8_3 | V8_4 | V8_5 | V8_6 | Current
@@ -69,9 +81,12 @@ val version_strictly_greater : compat_version -> bool
val version_less_or_equal : compat_version -> bool
val pr_version : compat_version -> string
+(* Beautify command line flags, should move to printing? *)
val beautify : bool ref
val beautify_file : bool ref
+(* Silent/verbose, both actually controlled by a single flag so they
+ are mutually exclusive *)
val make_silent : bool -> unit
val is_silent : unit -> bool
val is_verbose : unit -> bool
@@ -80,6 +95,7 @@ val verbosely : ('a -> 'b) -> 'a -> 'b
val if_silent : ('a -> unit) -> 'a -> unit
val if_verbose : ('a -> unit) -> 'a -> unit
+(* Miscellaneus flags for vernac *)
val make_auto_intros : bool -> unit
val is_auto_intros : unit -> bool
@@ -111,10 +127,6 @@ val without_option : bool ref -> ('a -> 'b) -> 'a -> 'b
(** Temporarily extends the reference to a list *)
val with_extra_values : 'c list ref -> 'c list -> ('a -> 'b) -> 'a -> 'b
-(** If [None], no limit *)
-val set_print_hyps_limit : int option -> unit
-val print_hyps_limit : unit -> int option
-
(** Options for external tools *)
(** Returns string format for default browser to use from Coq or CoqIDE *)
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index 58123f63e..bcb28f77c 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -374,7 +374,7 @@ let data = ref SM.empty
let _ =
Feedback.(add_feeder (function
- | { id = State s; contents = Custom (_, "ltacprof_results", xml) } ->
+ | { id = s; contents = Custom (_, "ltacprof_results", xml) } ->
let results = to_ltacprof_results xml in
let other_results = (* Multi success can cause this *)
try SM.find s !data
diff --git a/printing/printer.ml b/printing/printer.ml
index 239e1d7eb..35ddf2e8c 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -375,8 +375,21 @@ let pr_context_limit_compact ?n env sigma =
let pr_context_unlimited_compact env sigma =
pr_context_limit_compact env sigma
-let pr_context_of env sigma =
- match Flags.print_hyps_limit () with
+(* The number of printed hypothesis in a goal *)
+(* If [None], no limit *)
+let print_hyps_limit = ref (None : int option)
+
+let _ =
+ let open Goptions in
+ declare_int_option
+ { optsync = false;
+ optdepr = false;
+ optname = "the hypotheses limit";
+ optkey = ["Hyps";"Limit"];
+ optread = (fun () -> !print_hyps_limit);
+ optwrite = (fun x -> print_hyps_limit := x) }
+
+let pr_context_of env sigma = match !print_hyps_limit with
| None -> hv 0 (pr_context_limit_compact env sigma)
| Some n -> hv 0 (pr_context_limit_compact ~n env sigma)
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 125491988..3459156a4 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -105,7 +105,7 @@ module Make(T : Task) = struct
let report_status ?(id = !Flags.async_proofs_worker_id) s =
let open Feedback in
- feedback ~id:(State Stateid.initial) (WorkerStatus(id, s))
+ feedback ~id:Stateid.initial (WorkerStatus(id, s))
module Worker = Spawn.Sync(struct end)
diff --git a/stm/stm.ml b/stm/stm.ml
index 2b6ee5511..fd264e404 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -6,34 +6,32 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+(* enable in case of stm problems *)
+let stm_debug = false
+
let stm_pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr
let stm_pp_err pp = Format.eprintf "%s] @[%a@]\n" (System.process_id ()) Pp.pp_with pp; flush stderr
-let stm_prerr_endline s = if false then begin stm_pr_err (s ()) end else ()
-let stm_prerr_debug s = if !Flags.debug then begin stm_pr_err (s ()) end else ()
+let stm_prerr_endline s = if stm_debug then begin stm_pr_err (s ()) end else ()
+let stm_pperr_endline s = if stm_debug then begin stm_pp_err (s ()) end else ()
-let stm_pperr_endline s = if false then begin stm_pp_err (s ()) end else ()
+let stm_prerr_debug s = if !Flags.debug then begin stm_pr_err (s ()) end else ()
-open Vernacexpr
-open CErrors
open Pp
-open Names
-open Util
-open Ppvernac
-open Vernac_classifier
+open CErrors
open Feedback
+open Vernacexpr
+open Vernac_classifier
let execution_error state_id loc msg =
- feedback ~id:(State state_id)
+ feedback ~id:state_id
(Message (Error, Some loc, msg))
module Hooks = struct
-let process_error, process_error_hook = Hook.make ()
-
let state_computed, state_computed_hook = Hook.make
~default:(fun state_id ~in_cache ->
- feedback ~id:(State state_id) Processed) ()
+ feedback ~id:state_id Processed) ()
let state_ready, state_ready_hook = Hook.make
~default:(fun state_id -> ()) ()
@@ -45,16 +43,9 @@ let forward_feedback, forward_feedback_hook =
try Mutex.lock m; feedback ~id:id ~route contents; Mutex.unlock m
with e -> Mutex.unlock m; raise e) ()
-let parse_error, parse_error_hook = Hook.make
- ~default:(fun id loc msg ->
- feedback ~id (Message(Error, Some loc, msg))) ()
-
let unreachable_state, unreachable_state_hook = Hook.make
~default:(fun _ _ -> ()) ()
-let tactic_being_run, tactic_being_run_hook = Hook.make
- ~default:(fun _ -> ()) ()
-
include Hook
(* enables: Hooks.(call foo args) *)
@@ -66,7 +57,7 @@ let call_process_error_once =
match Exninfo.get info processed with
| Some _ -> ei
| None ->
- let e, info = call process_error ei in
+ let e, info = ExplainErr.process_vernac_interp_error ei in
let info = Exninfo.add info processed () in
e, info
@@ -86,7 +77,7 @@ type aast = {
strlen : int;
mutable expr : vernac_expr; (* mutable: Proof using hinted by aux file *)
}
-let pr_ast { expr; indentation } = int indentation ++ str " " ++ pr_vernac expr
+let pr_ast { expr; indentation } = Pp.(int indentation ++ str " " ++ Ppvernac.pr_vernac expr)
let default_proof_mode () = Proof_global.get_default_proof_mode_name ()
@@ -102,43 +93,6 @@ let may_pierce_opaque = function
| { expr = VernacExtend (("ExtractionInductive",_), _) } -> true
| _ -> false
-(* Wrapper for Vernac.parse_sentence to set the feedback id *)
-let indentation_of_string s =
- let len = String.length s in
- let rec aux n i precise =
- if i >= len then 0, precise, len
- else
- match s.[i] with
- | ' ' | '\t' -> aux (succ n) (succ i) precise
- | '\n' | '\r' -> aux 0 (succ i) true
- | _ -> n, precise, len in
- aux 0 0 false
-
-let vernac_parse ?(indlen_prev=fun() -> 0) ?newtip ?route eid s =
- let feedback_id =
- if Option.is_empty newtip then Edit eid
- else State (Option.get newtip) in
- let indentation, precise, strlen = indentation_of_string s in
- let indentation =
- if precise then indentation else indlen_prev () + indentation in
- set_id_for_feedback ?route feedback_id;
- let pa = Pcoq.Gram.parsable (Stream.of_string s) in
- Flags.with_option Flags.we_are_parsing (fun () ->
- try
- match Pcoq.Gram.entry_parse Pcoq.main_entry pa with
- | None -> raise (Invalid_argument "vernac_parse")
- | Some (loc, ast) -> indentation, strlen, loc, ast
- with e when CErrors.noncritical e ->
- let (e, info) = CErrors.push e in
- let loc = Option.default Loc.ghost (Loc.get_loc info) in
- Hooks.(call parse_error feedback_id loc (iprint (e, info)));
- iraise (e, info))
- ()
-
-let pr_open_cur_subgoals () =
- try Printer.pr_open_subgoals ()
- with Proof_global.NoCurrentProof -> Pp.str ""
-
let update_global_env () =
if Proof_global.there_are_pending_proofs () then
Proof_global.update_global_env ()
@@ -158,13 +112,13 @@ type cmd_t = {
ctac : bool; (* is a tactic *)
ceff : bool; (* is a side-effecting command in the middle of a proof *)
cast : aast;
- cids : Id.t list;
+ cids : Names.Id.t list;
cblock : proof_block_name option;
cqueue : [ `MainQueue
| `TacQueue of solving_tac * anon_abstracting_tac * cancel_switch
| `QueryQueue of cancel_switch
| `SkipQueue ] }
-type fork_t = aast * Vcs_.Branch.t * Vernacexpr.opacity_guarantee * Id.t list
+type fork_t = aast * Vcs_.Branch.t * Vernacexpr.opacity_guarantee * Names.Id.t list
type qed_t = {
qast : aast;
keep : vernac_qed_type;
@@ -253,7 +207,7 @@ end = struct (* {{{ *)
let proof_nesting vcs =
List.fold_left max 0
- (List.map_filter
+ (CList.map_filter
(function
| { Vcs_.kind = `Proof (_,n) } -> Some n
| { Vcs_.kind = `Edit _ } -> Some 1
@@ -369,6 +323,15 @@ end = struct (* {{{ *)
open Printf
let print_dag vcs () =
+
+ (* Due to threading, be wary that this will be called from the
+ toplevel with we_are_parsing set to true, as indeed, the
+ toplevel is waiting for input . What a race! XD
+
+ In case you are hitting the race enable stm_debug.
+ *)
+ if stm_debug then Flags.we_are_parsing := false;
+
let fname =
"stm_" ^ Str.global_replace (Str.regexp " ") "_" (System.process_id ()) in
let string_of_transaction = function
@@ -380,7 +343,7 @@ end = struct (* {{{ *)
| Sideff None -> "EnvChange"
| Noop -> " "
| Alias (id,_) -> sprintf "Alias(%s)" (Stateid.to_string id)
- | Qed { qast } -> string_of_ppcmds (pr_ast qast) in
+ | Qed { qast } -> Pp.string_of_ppcmds (pr_ast qast) in
let is_green id =
match get_info vcs id with
| Some { state = Valid _ } -> true
@@ -510,8 +473,8 @@ end = struct (* {{{ *)
let reachable id = reachable !vcs id
let mk_branch_name { expr = x } = Branch.make
(match x with
- | VernacDefinition (_,((_,i),_),_) -> string_of_id i
- | VernacStartTheoremProof (_,[Some ((_,i),_),_],_) -> string_of_id i
+ | VernacDefinition (_,((_,i),_),_) -> Names.string_of_id i
+ | VernacStartTheoremProof (_,[Some ((_,i),_),_],_) -> Names.string_of_id i
| _ -> "branch")
let edit_branch = Branch.make "edit"
let branch ?root ?pos name kind = vcs := branch !vcs ?root ?pos name kind
@@ -567,7 +530,7 @@ end = struct (* {{{ *)
| { next = n; step = `Alias x } -> (id,Alias x) :: aux n
| { next = n; step = `Sideff (`Ast (x,_)) } ->
(id,Sideff (Some x)) :: aux n
- | _ -> anomaly(str("Cannot slice from "^ Stateid.to_string block_start ^
+ | _ -> anomaly Pp.(str("Cannot slice from "^ Stateid.to_string block_start ^
" to "^Stateid.to_string block_stop))
in aux block_stop
@@ -620,11 +583,11 @@ end = struct (* {{{ *)
l
let create_proof_task_box l ~qed ~block_start:lemma =
- if not (topo_invariant l) then anomaly (str "overlapping boxes");
+ if not (topo_invariant l) then anomaly Pp.(str "overlapping boxes");
vcs := create_property !vcs l (ProofTask { qed; lemma })
let create_proof_block ({ block_start; block_stop} as decl) name =
let l = nodes_in_slice ~block_start ~block_stop in
- if not (topo_invariant l) then anomaly (str "overlapping boxes");
+ if not (topo_invariant l) then anomaly Pp.(str "overlapping boxes");
vcs := create_property !vcs l (ProofBlock (decl, name))
let box_of id = List.map Dag.Property.data (property_of !vcs id)
let delete_boxes_of id =
@@ -635,7 +598,7 @@ end = struct (* {{{ *)
with
| [] -> None
| [x] -> Some x
- | _ -> anomaly (str "node with more than 1 proof task box")
+ | _ -> anomaly Pp.(str "node with more than 1 proof task box")
let gc () =
let old_vcs = !vcs in
@@ -716,14 +679,14 @@ module State : sig
?safe_id:Stateid.t ->
?redefine:bool -> ?cache:Summary.marshallable ->
?feedback_processed:bool -> (unit -> unit) -> Stateid.t -> unit
- val fix_exn_ref : (iexn -> iexn) ref
+ val fix_exn_ref : (Exninfo.iexn -> Exninfo.iexn) ref
val install_cached : Stateid.t -> unit
val is_cached : ?cache:Summary.marshallable -> Stateid.t -> bool
val is_cached_and_valid : ?cache:Summary.marshallable -> Stateid.t -> bool
- val exn_on : Stateid.t -> valid:Stateid.t -> iexn -> iexn
+ val exn_on : Stateid.t -> valid:Stateid.t -> Exninfo.iexn -> Exninfo.iexn
(* to send states across worker/master *)
type frozen_state
val get_cached : Stateid.t -> frozen_state
@@ -736,6 +699,9 @@ module State : sig
val proof_part_of_frozen : frozen_state -> proof_part
val assign : Stateid.t -> partial_state -> unit
+ (* Only for internal use to catch problems in parse_sentence, should
+ be removed in the state handling refactoring. *)
+ val cur_id : Stateid.t ref
end = struct (* {{{ *)
(* cur_id holds Stateid.dummy in case the last attempt to define a state
@@ -796,13 +762,13 @@ end = struct (* {{{ *)
| _ ->
(* coqc has a 1 slot cache and only for valid states *)
if interactive () = `No && Stateid.equal id !cur_id then ()
- else anomaly (str "installing a non cached state")
+ else anomaly Pp.(str "installing a non cached state")
let get_cached id =
try match VCS.get_info id with
| { state = Valid s } -> s
- | _ -> anomaly (str "not a cached state")
- with VCS.Expired -> anomaly (str "not a cached state (expired)")
+ | _ -> anomaly Pp.(str "not a cached state")
+ with VCS.Expired -> anomaly Pp.(str "not a cached state (expired)")
let assign id what =
if VCS.get_state id <> Empty then () else
@@ -850,10 +816,10 @@ end = struct (* {{{ *)
let define ?safe_id ?(redefine=false) ?(cache=`No) ?(feedback_processed=true)
f id
=
- feedback ~id:(State id) (ProcessingIn !Flags.async_proofs_worker_id);
+ feedback ~id:id (ProcessingIn !Flags.async_proofs_worker_id);
let str_id = Stateid.to_string id in
if is_cached id && not redefine then
- anomaly (str"defining state "++str str_id++str" twice");
+ anomaly Pp.(str"defining state "++str str_id++str" twice");
try
stm_prerr_endline (fun () -> "defining "^str_id^" (cache="^
if cache = `Yes then "Y)" else if cache = `Shallow then "S)" else "N)");
@@ -928,9 +894,9 @@ let indent_script_item ((ng1,ngl1),nl,beginend,ppl) (cmd,ng) =
| VernacBullet _ -> pred ind, nl, beginend
| _ -> ind, nl, beginend
in
- let pp =
+ let pp = Pp.(
(if nl then fnl () else mt ()) ++
- (hov (ind+1) (str (String.make ind ' ') ++ Ppvernac.pr_vernac cmd))
+ (hov (ind+1) (str (String.make ind ' ') ++ Ppvernac.pr_vernac cmd)))
in
(new_ngl, new_nl, new_beginend, pp :: ppl)
@@ -970,7 +936,7 @@ let show_script ?proof () =
List.fold_left indent_script_item ((1,[]),false,[],[]) cmds
in
let indented_cmds = List.rev (indented_cmds) in
- msg_notice (v 0 (prlist_with_sep fnl (fun x -> x) indented_cmds))
+ msg_notice Pp.(v 0 (prlist_with_sep fnl (fun x -> x) indented_cmds))
with Vcs_aux.Expired -> ()
end
@@ -982,7 +948,7 @@ let stm_vernac_interp ?proof id ?route { verbose; loc; expr } =
(* The Stm will gain the capability to interpret commmads affecting
the whole document state, such as backtrack, etc... so we start
to design the stm command interpreter now *)
- set_id_for_feedback ?route (State id);
+ set_id_for_feedback ?route id;
Aux_file.record_in_aux_set_at loc;
(* We need to check if a command should be filtered from
* vernac_entries, as it cannot handle it. This should go away in
@@ -997,15 +963,15 @@ let stm_vernac_interp ?proof id ?route { verbose; loc; expr } =
in
let aux_interp cmd =
if is_filtered_command cmd then
- stm_pperr_endline Pp.(fun () -> str "ignoring " ++ pr_vernac expr)
+ stm_pperr_endline Pp.(fun () -> str "ignoring " ++ Ppvernac.pr_vernac expr)
else match cmd with
| VernacShow ShowScript -> ShowScript.show_script ()
| expr ->
- stm_pperr_endline Pp.(fun () -> str "interpreting " ++ pr_vernac expr);
+ stm_pperr_endline Pp.(fun () -> str "interpreting " ++ Ppvernac.pr_vernac expr);
try Vernacentries.interp ?verbosely:(Some verbose) ?proof (loc, expr)
with e ->
let e = CErrors.push e in
- iraise Hooks.(call_process_error_once e)
+ Exninfo.iraise Hooks.(call_process_error_once e)
in aux_interp expr
(****************************** CRUFT *****************************************)
@@ -1016,7 +982,6 @@ module Backtrack : sig
val record : unit -> unit
val backto : Stateid.t -> unit
- val back_safe : unit -> unit
(* we could navigate the dag, but this ways easy *)
val branches_of : Stateid.t -> backup
@@ -1045,7 +1010,7 @@ end = struct (* {{{ *)
let info = VCS.get_info oid in
match info.vcs_backup with
| None, _ ->
- anomaly(str"Backtrack.backto "++str(Stateid.to_string oid)++
+ anomaly Pp.(str"Backtrack.backto "++str(Stateid.to_string oid)++
str": a state with no vcs_backup")
| Some vcs, _ -> VCS.restore vcs
@@ -1053,8 +1018,8 @@ end = struct (* {{{ *)
let info = VCS.get_info id in
match info.vcs_backup with
| _, None ->
- anomaly(str"Backtrack.branches_of "++str(Stateid.to_string id)++
- str": a state with no vcs_backup")
+ anomaly Pp.(str"Backtrack.branches_of "++str(Stateid.to_string id)++
+ str": a state with no vcs_backup")
| _, Some x -> x
let rec fold_until f acc id =
@@ -1115,7 +1080,7 @@ end = struct (* {{{ *)
let id = VCS.get_branch_pos (VCS.current_branch ()) in
let vcs =
match (VCS.get_info id).vcs_backup with
- | None, _ -> anomaly(str"Backtrack: tip with no vcs_backup")
+ | None, _ -> anomaly Pp.(str"Backtrack: tip with no vcs_backup")
| Some vcs, _ -> vcs in
let cb, _ =
try Vcs_aux.find_proof_at_depth vcs (Vcs_aux.proof_nesting vcs)
@@ -1139,7 +1104,7 @@ end = struct (* {{{ *)
with
| Not_found ->
CErrors.user_err ~hdr:"undo_vernac_classifier"
- (str "Cannot undo")
+ Pp.(str "Cannot undo")
end (* }}} *)
@@ -1171,7 +1136,7 @@ let record_pb_time proof_name loc time =
hints := Aux_file.set !hints Loc.ghost proof_name proof_build_time
end
-exception RemoteException of std_ppcmds
+exception RemoteException of Pp.std_ppcmds
let _ = CErrors.register_handler (function
| RemoteException ppcmd -> ppcmd
| _ -> raise Unhandled)
@@ -1206,7 +1171,7 @@ let proof_block_delimiters = ref []
let register_proof_block_delimiter name static dynamic =
if List.mem_assoc name !proof_block_delimiters then
- CErrors.user_err ~hdr:"STM" (str "Duplicate block delimiter " ++ str name);
+ CErrors.user_err ~hdr:"STM" Pp.(str "Duplicate block delimiter " ++ str name);
proof_block_delimiters := (name, (static,dynamic)) :: !proof_block_delimiters
let mk_doc_node id = function
@@ -1242,7 +1207,7 @@ let detect_proof_block id name =
end
with Not_found ->
CErrors.user_err ~hdr:"STM"
- (str "Unknown proof block delimiter " ++ str name)
+ Pp.(str "Unknown proof block delimiter " ++ str name)
)
(****************************** THE SCHEDULER *********************************)
(******************************************************************************)
@@ -1309,7 +1274,7 @@ end = struct (* {{{ *)
type error = {
e_error_at : Stateid.t;
e_safe_id : Stateid.t;
- e_msg : std_ppcmds;
+ e_msg : Pp.std_ppcmds;
e_safe_states : Stateid.t list }
type response =
@@ -1382,9 +1347,9 @@ end = struct (* {{{ *)
| Some (BuildProof { t_start = start; t_assign }) ->
let s = "Worker dies or task expired" in
let info = Stateid.add ~valid:start Exninfo.null start in
- let e = (RemoteException (strbrk s), info) in
+ let e = (RemoteException (Pp.strbrk s), info) in
t_assign (`Exn e);
- execution_error start Loc.ghost (strbrk s);
+ execution_error start Loc.ghost (Pp.strbrk s);
feedback (InProgress ~-1)
let build_proof_here ~drop_pt (id,valid) loc eop =
@@ -1396,7 +1361,7 @@ end = struct (* {{{ *)
Aux_file.record_in_aux_at loc "proof_build_time"
(Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
let p = Proof_global.return_proof ~allow_partial:drop_pt () in
- if drop_pt then feedback ~id:(State id) Complete;
+ if drop_pt then feedback ~id Complete;
p)
let perform_buildp { Stateid.exn_info; stop; document; loc } drop my_states =
@@ -1465,7 +1430,7 @@ end = struct (* {{{ *)
when is_tac expr && State.same_env o n -> (* A pure tactic *)
Some (id, `Proof (prev, State.proof_part_of_frozen n))
| Some _, Some s ->
- msg_debug (str "STM: sending back a fat state");
+ msg_debug (Pp.str "STM: sending back a fat state");
Some (id, `Full s)
| _, Some s -> Some (id, `Full s) in
let rec aux seen = function
@@ -1481,10 +1446,10 @@ end = struct (* {{{ *)
| ReqStates sl -> RespStates (perform_states sl)
let on_marshal_error s = function
- | States _ -> msg_error(strbrk("Marshalling error: "^s^". "^
+ | States _ -> msg_error(Pp.strbrk("Marshalling error: "^s^". "^
"The system state could not be sent to the master process."))
| BuildProof { t_exn_info; t_stop; t_assign; t_loc; t_drop = drop_pt } ->
- msg_error(strbrk("Marshalling error: "^s^". "^
+ msg_error(Pp.strbrk("Marshalling error: "^s^". "^
"The system state could not be sent to the worker process. "^
"Falling back to local, lazy, evaluation."));
t_assign(`Comp(build_proof_here ~drop_pt t_exn_info t_loc t_stop));
@@ -1537,7 +1502,7 @@ end = struct (* {{{ *)
let check_task_aux extra name l i =
let { Stateid.stop; document; loc; name = r_name }, drop = List.nth l i in
Flags.if_verbose msg_info
- (str(Printf.sprintf "Checking task %d (%s%s) of %s" i r_name extra name));
+ Pp.(str(Printf.sprintf "Checking task %d (%s%s) of %s" i r_name extra name));
VCS.restore document;
let start =
let rec aux cur =
@@ -1568,7 +1533,7 @@ end = struct (* {{{ *)
let (e, info) = CErrors.push e in
(try match Stateid.get info with
| None ->
- msg_error (
+ msg_error Pp.(
str"File " ++ str name ++ str ": proof of " ++ str r_name ++
spc () ++ iprint (e, info))
| Some (_, cur) ->
@@ -1578,16 +1543,16 @@ end = struct (* {{{ *)
| { step = `Qed ( { qast = { loc } }, _) }
| { step = `Sideff (`Ast ( { loc }, _)) } ->
let start, stop = Loc.unloc loc in
- msg_error (
+ msg_error Pp.(
str"File " ++ str name ++ str ": proof of " ++ str r_name ++
str ": chars " ++ int start ++ str "-" ++ int stop ++
spc () ++ iprint (e, info))
| _ ->
- msg_error (
+ msg_error Pp.(
str"File " ++ str name ++ str ": proof of " ++ str r_name ++
spc () ++ iprint (e, info))
with e ->
- msg_error (str"unable to print error message: " ++
+ msg_error Pp.(str"unable to print error message: " ++
str (Printexc.to_string e)));
if drop then `ERROR_ADMITTED else `ERROR
@@ -1746,7 +1711,7 @@ end = struct (* {{{ *)
type response =
| RespBuiltSubProof of output
- | RespError of std_ppcmds
+ | RespError of Pp.std_ppcmds
| RespNoProgress
exception NoProgress
@@ -1806,7 +1771,7 @@ end = struct (* {{{ *)
List.for_all (Context.Named.Declaration.for_all is_ground)
Evd.(evar_context g))
then
- CErrors.user_err ~hdr:"STM" (strbrk("the par: goal selector supports ground "^
+ CErrors.user_err ~hdr:"STM" Pp.(strbrk("the par: goal selector supports ground "^
"goals only"))
else begin
let (i, ast) = r_ast in
@@ -1821,7 +1786,7 @@ end = struct (* {{{ *)
if Evarutil.is_ground_term sigma t then
let t = EConstr.Unsafe.to_constr t in
RespBuiltSubProof (t, Evd.evar_universe_context sigma)
- else CErrors.user_err ~hdr:"STM" (str"The solution is not ground")
+ else CErrors.user_err ~hdr:"STM" Pp.(str"The solution is not ground")
end) ()
with e when CErrors.noncritical e -> RespError (CErrors.print e)
@@ -1943,11 +1908,11 @@ end = struct (* {{{ *)
Reach.known_state ~cache:`No r_where;
try
stm_vernac_interp r_for { r_what with verbose = true };
- feedback ~id:(State r_for) Processed
+ feedback ~id:r_for Processed
with e when CErrors.noncritical e ->
let e = CErrors.push e in
let msg = iprint e in
- feedback ~id:(State r_for) (Message (Error, None, msg))
+ feedback ~id:r_for (Message (Error, None, msg))
let name_of_task { t_what } = string_of_ppcmds (pr_ast t_what)
let name_of_request { r_what } = string_of_ppcmds (pr_ast r_what)
@@ -2009,7 +1974,7 @@ let collect_proof keep cur hd brkind id =
let no_name = "" in
let name = function
| [] -> no_name
- | id :: _ -> Id.to_string id in
+ | id :: _ -> Names.Id.to_string id in
let loc = (snd cur).loc in
let is_defined = function
| _, { expr = VernacEndProof (Proved ((Transparent|Opaque (Some _)),_)) } ->
@@ -2130,13 +2095,13 @@ let known_state ?(redefine_qed=false) ~cache id =
Some (decl, name)
| _ -> None) boxes in
assert(List.length valid_boxes < 2);
- if valid_boxes = [] then iraise exn
+ if valid_boxes = [] then Exninfo.iraise exn
else
let decl, name = List.hd valid_boxes in
try
let _, dynamic_check = List.assoc name !proof_block_delimiters in
match dynamic_check decl with
- | `Leaks -> iraise exn
+ | `Leaks -> Exninfo.iraise exn
| `ValidBlock { base_state; goals_to_admit; recovery_command } -> begin
let tac =
let open Proofview.Notations in
@@ -2149,7 +2114,7 @@ let known_state ?(redefine_qed=false) ~cache id =
| Valid { proof } ->
Proof_global.unfreeze proof;
Proof_global.with_current_proof (fun _ p ->
- feedback ~id:(State id) Feedback.AddedAxiom;
+ feedback ~id:id Feedback.AddedAxiom;
fst (Pfedit.solve Vernacexpr.SelectAll None tac p), ());
Option.iter (fun expr -> stm_vernac_interp id {
verbose = true; loc = Loc.ghost; expr; indentation = 0;
@@ -2216,10 +2181,8 @@ let known_state ?(redefine_qed=false) ~cache id =
(fun () ->
resilient_tactic id cblock (fun () ->
reach ~cache:`Shallow view.next;
- Hooks.(call tactic_being_run true);
Partac.vernac_interp ~solve ~abstract
- cancel !Flags.async_proofs_n_tacworkers view.next id x;
- Hooks.(call tactic_being_run false))
+ cancel !Flags.async_proofs_n_tacworkers view.next id x)
), cache, true
| `Cmd { cast = x; cqueue = `QueryQueue cancel }
when Flags.async_proofs_is_master () -> (fun () ->
@@ -2229,9 +2192,7 @@ let known_state ?(redefine_qed=false) ~cache id =
| `Cmd { cast = x; ceff = eff; ctac = true; cblock } -> (fun () ->
resilient_tactic id cblock (fun () ->
reach view.next;
- Hooks.(call tactic_being_run true);
- stm_vernac_interp id x;
- Hooks.(call tactic_being_run false));
+ stm_vernac_interp id x);
if eff then update_global_env ()
), (if eff then `Yes else cache), true
| `Cmd { cast = x; ceff = eff } -> (fun () ->
@@ -2254,7 +2215,7 @@ let known_state ?(redefine_qed=false) ~cache id =
with e when CErrors.noncritical e ->
let (e, info) = CErrors.push e in
let info = Stateid.add info ~valid:prev id in
- iraise (e, info));
+ Exninfo.iraise (e, info));
wall_clock_last_fork := Unix.gettimeofday ()
), `Yes, true
| `Qed ({ qast = x; keep; brinfo; brname } as qed, eop) ->
@@ -2301,7 +2262,7 @@ let known_state ?(redefine_qed=false) ~cache id =
if not delegate then ignore(Future.compute fp);
reach view.next;
stm_vernac_interp id ~proof x;
- feedback ~id:(State id) Incomplete
+ feedback ~id:id Incomplete
| { VCS.kind = `Master }, _ -> assert false
end;
Proof_global.discard_all ()
@@ -2337,9 +2298,9 @@ let known_state ?(redefine_qed=false) ~cache id =
| `MaybeASync (start, pua, nodes, name, delegate) -> (fun () ->
reach ~cache:`Shallow start;
(* no sections *)
- if List.is_empty (Environ.named_context (Global.env ()))
- then pi1 (aux (`ASync (start, pua, nodes, name, delegate))) ()
- else pi1 (aux (`Sync (name, pua, `NoPU_NoHint_NoES))) ()
+ if CList.is_empty (Environ.named_context (Global.env ()))
+ then Util.pi1 (aux (`ASync (start, pua, nodes, name, delegate))) ()
+ else Util.pi1 (aux (`Sync (name, pua, `NoPU_NoHint_NoES))) ()
), (if redefine_qed then `No else `Yes), true
in
aux (collect_proof keep (view.next, x) brname brinfo eop)
@@ -2393,20 +2354,20 @@ let observe id =
let e = CErrors.push e in
VCS.print ();
VCS.restore vcs;
- iraise e
+ Exninfo.iraise e
-let finish ?(print_goals=false) () =
+let finish () =
let head = VCS.current_branch () in
observe (VCS.get_branch_pos head);
- if print_goals then msg_notice (pr_open_cur_subgoals ());
VCS.print ();
+ (* EJGA: Setting here the proof state looks really wrong, and it
+ hides true bugs cf bug #5363. Also, what happens with observe? *)
(* Some commands may by side effect change the proof mode *)
match VCS.get_branch head with
| { VCS.kind = `Edit (mode,_,_,_,_) } -> Proof_global.activate_proof_mode mode
| { VCS.kind = `Proof (mode, _) } -> Proof_global.activate_proof_mode mode
| _ -> ()
-
let wait () =
Slaves.wait_all_done ();
VCS.print ()
@@ -2480,35 +2441,23 @@ let merge_proof_branch ~valid ?id qast keep brname =
VCS.checkout VCS.Branch.master;
`Unfocus qed_id
| { VCS.kind = `Master } ->
- iraise (State.exn_on ~valid Stateid.dummy (Proof_global.NoCurrentProof, Exninfo.null))
+ Exninfo.iraise (State.exn_on ~valid Stateid.dummy (Proof_global.NoCurrentProof, Exninfo.null))
(* When tty is true, this code also does some of the job of the user interface:
jump back to a state that is valid *)
-let handle_failure (e, info) vcs tty =
- if e = CErrors.Drop then iraise (e, info) else
+let handle_failure (e, info) vcs =
+ if e = CErrors.Drop then Exninfo.iraise (e, info) else
match Stateid.get info with
| None ->
VCS.restore vcs;
VCS.print ();
- if tty && interactive () = `Yes then begin
- (* Hopefully the 1 to last state is valid *)
- Backtrack.back_safe ();
- VCS.checkout_shallowest_proof_branch ();
- end;
- VCS.print ();
anomaly(str"error with no safe_id attached:" ++ spc() ++
CErrors.iprint_no_report (e, info))
| Some (safe_id, id) ->
stm_prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id);
VCS.restore vcs;
- if tty && interactive () = `Yes then begin
- (* We stay on a valid state *)
- Backtrack.backto safe_id;
- VCS.checkout_shallowest_proof_branch ();
- Reach.known_state ~cache:(interactive ()) safe_id;
- end;
VCS.print ();
- iraise (e, info)
+ Exninfo.iraise (e, info)
let snapshot_vio ldir long_f_dot_vo =
finish ();
@@ -2520,7 +2469,7 @@ let snapshot_vio ldir long_f_dot_vo =
let reset_task_queue = Slaves.reset_task_queue
(* Document building *)
-let process_transaction ?(newtip=Stateid.fresh ()) ~tty
+let process_transaction ?(newtip=Stateid.fresh ())
({ verbose; loc; expr } as x) c =
stm_pperr_endline (fun () -> str "{{{ processing: " ++ pr_ast x);
let vcs = VCS.backup () in
@@ -2566,18 +2515,11 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
anomaly(str"classifier: VtBack + VtLater must imply part_of_script")
(* Query *)
- | VtQuery (false,(report_id,route)), VtNow when tty = true ->
- finish ();
- (try Future.purify (stm_vernac_interp report_id ~route)
- {x with verbose = true }
- with e when CErrors.noncritical e ->
- let e = CErrors.push e in
- iraise (State.exn_on ~valid:Stateid.dummy report_id e)); `Ok
| VtQuery (false,(report_id,route)), VtNow ->
(try stm_vernac_interp report_id ~route x
with e ->
let e = CErrors.push e in
- iraise (State.exn_on ~valid:Stateid.dummy report_id e)); `Ok
+ Exninfo.iraise (State.exn_on ~valid:Stateid.dummy report_id e)); `Ok
| VtQuery (true,(report_id,_)), w ->
assert(Stateid.equal report_id Stateid.dummy);
let id = VCS.new_node ~id:newtip () in
@@ -2704,7 +2646,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
rc
with e ->
let e = CErrors.push e in
- handle_failure e vcs tty
+ handle_failure e vcs
let get_ast id =
match VCS.visit id with
@@ -2716,29 +2658,94 @@ let get_ast id =
let stop_worker n = Slaves.cancel_worker n
+(* We must parse on top of a state id, it should be something like:
+
+ - get parsing information for that state.
+ - feed the parsable / parser with the right parsing information.
+ - call the parser
+
+ Now, the invariant in ensured by the callers, but this is a bit
+ problematic.
+*)
+exception End_of_input
+
+let parse_sentence sid pa =
+ (* XXX: Should this restore the previous state?
+ Using reach here to try to really get to the
+ proper state makes the error resilience code fail *)
+ (* Reach.known_state ~cache:`Yes sid; *)
+ let cur_tip = VCS.cur_tip () in
+ let real_tip = !State.cur_id in
+ if not (Stateid.equal sid cur_tip) then
+ user_err ~hdr:"Stm.parse_sentence"
+ (str "Currently, the parsing api only supports parsing at the tip of the document." ++ fnl () ++
+ str "You wanted to parse at: " ++ str (Stateid.to_string sid) ++
+ str " but the current tip is: " ++ str (Stateid.to_string cur_tip)) ;
+ if not (Stateid.equal sid real_tip) && !Flags.debug && stm_debug then
+ Feedback.msg_debug
+ (str "Warning, the real tip doesn't match the current tip." ++
+ str "You wanted to parse at: " ++ str (Stateid.to_string sid) ++
+ str " but the real tip is: " ++ str (Stateid.to_string real_tip) ++ fnl () ++
+ str "This is usually due to use of Stm.observe to evaluate a state different than the tip. " ++
+ str "All is good if not parsing changes occur between the two states, however if they do, a problem might occur.");
+ Flags.with_option Flags.we_are_parsing (fun () ->
+ try
+ match Pcoq.Gram.entry_parse Pcoq.main_entry pa with
+ | None -> raise End_of_input
+ | Some com -> com
+ with e when CErrors.noncritical e ->
+ let (e, info) = CErrors.push e in
+ Exninfo.iraise (e, info))
+ ()
+
(* You may need to know the len + indentation of previous command to compute
* the indentation of the current one.
* Eg. foo. bar.
* Here bar is indented of the indentation of foo + its strlen (4) *)
-let ind_len_of id =
- if Stateid.equal id Stateid.initial then 0
- else match (VCS.visit id).step with
- | `Cmd { ctac = true; cast = { indentation; strlen } } ->
- indentation + strlen
- | _ -> 0
-
-let add ~ontop ?newtip ?(check=ignore) verb eid s =
+let ind_len_loc_of_id sid =
+ if Stateid.equal sid Stateid.initial then None
+ else match (VCS.visit sid).step with
+ | `Cmd { ctac = true; cast = { indentation; strlen; loc } } ->
+ Some (indentation, strlen, loc)
+ | _ -> None
+
+(* the indentation logic works like this: if the beginning of the
+ command is different than the start we are in a new line, thus
+ indentation follows from the starting position. Otherwise, we use
+ the previous one plus the offset.
+
+ Note, this could maybe improved by handling more cases in
+ compute_indentation. *)
+
+let compute_indentation sid loc =
+ let open Loc in
+ (* The effective lenght is the lenght on the last line *)
+ let len = loc.ep - loc.bp in
+ let prev_indent = match ind_len_loc_of_id sid with
+ | None -> 0
+ | Some (i,l,p) -> i + l
+ in
+ (* Now if the line has not changed, the need to add the previous indent *)
+ let eff_indent = loc.bp - loc.bol_pos in
+ if loc.bol_pos = 0 then
+ eff_indent + prev_indent, len
+ else
+ eff_indent, len
+
+
+let add ~ontop ?newtip verb (loc, ast) =
let cur_tip = VCS.cur_tip () in
if not (Stateid.equal ontop cur_tip) then
- (* For now, arbitrary edits should be announced with edit_at *)
- anomaly(str"Not yet implemented, the GUI should not try this");
- let indentation, strlen, loc, ast =
- vernac_parse ~indlen_prev:(fun () -> ind_len_of ontop) ?newtip eid s in
+ user_err ~hdr:"Stm.add"
+ (str "Stm.add called for a different state (" ++ str (Stateid.to_string ontop) ++
+ str ") than the tip: " ++ str (Stateid.to_string cur_tip) ++ str "." ++ fnl () ++
+ str "This is not supported yet, sorry.");
+ let indentation, strlen = compute_indentation ontop loc in
CWarnings.set_current_loc loc;
- check(loc,ast);
+ (* XXX: Classifiy vernac should be moved inside process transaction *)
let clas = classify_vernac ast in
let aast = { verbose = verb; indentation; strlen; loc; expr = ast } in
- match process_transaction ?newtip ~tty:false aast clas with
+ match process_transaction ?newtip aast clas with
| `Ok -> VCS.cur_tip (), `NewTip
| `Unfocus qed_id -> qed_id, `Unfocus (VCS.cur_tip ())
@@ -2754,17 +2761,16 @@ let query ~at ?(report_with=(Stateid.dummy,default_route)) s =
Future.purify (fun s ->
if Stateid.equal at Stateid.dummy then finish ()
else Reach.known_state ~cache:`Yes at;
- let newtip, route = report_with in
- let indentation, strlen, loc, ast = vernac_parse ~newtip ~route 0 s in
+ let loc, ast = parse_sentence at s in
+ let indentation, strlen = compute_indentation at loc in
CWarnings.set_current_loc loc;
let clas = classify_vernac ast in
let aast = { verbose = true; indentation; strlen; loc; expr = ast } in
match clas with
| VtStm (w,_), _ ->
- ignore(process_transaction ~tty:false aast (VtStm (w,false), VtNow))
+ ignore(process_transaction aast (VtStm (w,false), VtNow))
| _ ->
- ignore(process_transaction
- ~tty:false aast (VtQuery (false,report_with), VtNow)))
+ ignore(process_transaction aast (VtQuery (false,report_with), VtNow)))
s
let edit_at id =
@@ -2888,37 +2894,16 @@ let edit_at id =
stm_prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id);
VCS.restore vcs;
VCS.print ();
- iraise (e, info)
+ Exninfo.iraise (e, info)
let backup () = VCS.backup ()
let restore d = VCS.restore d
+let get_current_state () = VCS.cur_tip ()
+
(*********************** TTY API (PG, coqtop, coqc) ***************************)
(******************************************************************************)
-let interp verb (loc,e) =
- let clas = classify_vernac e in
- let aast = { verbose = verb; indentation = 0; strlen = 0; loc; expr = e } in
- let rc = process_transaction ~tty:true aast clas in
- if rc <> `Ok then anomaly(str"tty loop can't be mixed with the STM protocol");
- if interactive () = `Yes ||
- (!Flags.async_proofs_mode = Flags.APoff &&
- !Flags.compilation_mode = Flags.BuildVo) then
- let vcs = VCS.backup () in
- let print_goals =
- verb && match clas with
- | VtQuery _, _ -> false
- | (VtProofStep _ | VtStm (VtBack _, _) | VtStartProof _), _ -> true
- | _ -> not !Flags.coqtop_ui in
- try finish ~print_goals ()
- with e ->
- let e = CErrors.push e in
- handle_failure e vcs true
-
-let finish () = finish ()
-
-let get_current_state () = VCS.cur_tip ()
-
let current_proof_depth () =
let head = VCS.current_branch () in
match VCS.get_branch head with
@@ -2939,15 +2924,13 @@ let proofname b = match VCS.get_branch b with
| _ -> None
let get_all_proof_names () =
- List.map unmangle (List.map_filter proofname (VCS.branches ()))
+ List.map unmangle (CList.map_filter proofname (VCS.branches ()))
(* Export hooks *)
let state_computed_hook = Hooks.state_computed_hook
let state_ready_hook = Hooks.state_ready_hook
-let parse_error_hook = Hooks.parse_error_hook
let forward_feedback_hook = Hooks.forward_feedback_hook
-let process_error_hook = Hooks.process_error_hook
let unreachable_state_hook = Hooks.unreachable_state_hook
let () = Hook.set Obligations.stm_get_fix_exn (fun () -> !State.fix_exn_ref)
-let tactic_being_run_hook = Hooks.tactic_being_run_hook
+
(* vim:set foldmethod=marker: *)
diff --git a/stm/stm.mli b/stm/stm.mli
index 0f0a3c4e1..30e9629c6 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -13,24 +13,31 @@ open Loc
(** state-transaction-machine interface *)
-(* [add ontop check vebose eid s] adds a new command [s] on the state [ontop]
- having edit id [eid]. [check] is called on the AST.
- The [ontop] parameter is just for asserting the GUI is on sync, but
- will eventually call edit_at on the fly if needed.
- The sentence [s] is parsed in the state [ontop].
- If [newtip] is provided, then the returned state id is guaranteed to be
- [newtip] *)
-val add :
- ontop:Stateid.t -> ?newtip:Stateid.t ->
- ?check:(vernac_expr located -> unit) ->
- bool -> edit_id -> string ->
- Stateid.t * [ `NewTip | `Unfocus of Stateid.t ]
-
-(* parses and executes a command at a given state, throws away its side effects
- but for the printings. Feedback is sent with report_with (defaults to dummy
- state id) *)
+(* [parse_sentence sid pa] Reads a sentence from [pa] with parsing
+ state [sid] Returns [End_of_input] if the stream ends *)
+val parse_sentence : Stateid.t -> Pcoq.Gram.coq_parsable ->
+ Vernacexpr.vernac_expr Loc.located
+
+(* Reminder: A parsable [pa] is constructed using
+ [Pcoq.Gram.coq_parsable stream], where [stream : char Stream.t]. *)
+
+exception End_of_input
+
+(* [add ~ontop ?newtip verbose cmd] adds a new command [cmd] ontop of
+ the state [ontop].
+ The [ontop] parameter just asserts that the GUI is on
+ sync, but it will eventually call edit_at on the fly if needed.
+ If [newtip] is provided, then the returned state id is guaranteed
+ to be [newtip] *)
+val add : ontop:Stateid.t -> ?newtip:Stateid.t ->
+ bool -> Vernacexpr.vernac_expr Loc.located ->
+ Stateid.t * [ `NewTip | `Unfocus of Stateid.t ]
+
+(* [query at ?report_with cmd] Executes [cmd] at a given state [at],
+ throwing away side effects except messages. Feedback will
+ be sent with [report_with], which defaults to the dummy state id *)
val query :
- at:Stateid.t -> ?report_with:(Stateid.t * Feedback.route_id) -> string -> unit
+ at:Stateid.t -> ?report_with:(Stateid.t * Feedback.route_id) -> Pcoq.Gram.coq_parsable -> unit
(* [edit_at id] is issued to change the editing zone. [`NewTip] is returned if
the requested id is the new document tip hence the document portion following
@@ -182,14 +189,10 @@ val register_proof_block_delimiter :
* the name of the Task(s) above) *)
val state_computed_hook : (Stateid.t -> in_cache:bool -> unit) Hook.t
-val parse_error_hook :
- (Feedback.edit_or_state_id -> Loc.t -> Pp.std_ppcmds -> unit) Hook.t
val unreachable_state_hook : (Stateid.t -> Exninfo.iexn -> unit) Hook.t
+
(* ready means that master has it at hand *)
val state_ready_hook : (Stateid.t -> unit) Hook.t
-(* called with true before and with false after a tactic explicitly
- * in the document is run *)
-val tactic_being_run_hook : (bool -> unit) Hook.t
(* Messages from the workers to the master *)
val forward_feedback_hook : (Feedback.feedback -> unit) Hook.t
@@ -202,16 +205,6 @@ type state = {
val state_of_id :
Stateid.t -> [ `Valid of state option | `Expired | `Error of exn ]
-(** read-eval-print loop compatible interface ****************************** **)
-
-(* Adds a new line to the document. It replaces the core of Vernac.interp.
- [finish] is called as the last bit of this function if the system
- is running interactively (-emacs or coqtop). *)
-val interp : bool -> vernac_expr located -> unit
-
(* Queries for backward compatibility *)
val current_proof_depth : unit -> int
val get_all_proof_names : unit -> Id.t list
-
-(* Hooks to be set by other Coq components in order to break file cycles *)
-val process_error_hook : Future.fix_exn Hook.t
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index ffd0d7805..2b9a04dad 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -27,12 +27,12 @@ let set_rcfile s = rcfile := s; rcfile_specified := true
let load_rc = ref true
let no_load_rc () = load_rc := false
-let load_rcfile() =
+let load_rcfile sid =
if !load_rc then
try
if !rcfile_specified then
if CUnix.file_readable_p !rcfile then
- Vernac.load_vernac false !rcfile
+ Vernac.load_vernac false sid !rcfile
else raise (Sys_error ("Cannot read rcfile: "^ !rcfile))
else
try
@@ -43,8 +43,8 @@ let load_rcfile() =
Envars.home ~warn / "."^rcdefaultname^"."^Coq_config.version;
Envars.home ~warn / "."^rcdefaultname
] in
- Vernac.load_vernac false inferedrc
- with Not_found -> ()
+ Vernac.load_vernac false sid inferedrc
+ with Not_found -> sid
(*
Flags.if_verbose
mSGNL (str ("No coqrc or coqrc."^Coq_config.version^
@@ -55,7 +55,8 @@ let load_rcfile() =
let () = Feedback.msg_info (str"Load of rcfile failed.") in
iraise reraise
else
- Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading.")
+ (Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading.");
+ sid)
(* Recursively puts dir in the LoadPath if -nois was not passed *)
let add_stdlib_path ~unix_path ~coq_root ~with_ml =
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index 4ff87628c..3b42289ee 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -13,7 +13,7 @@ val set_debug : unit -> unit
val set_rcfile : string -> unit
val no_load_rc : unit -> unit
-val load_rcfile : unit -> unit
+val load_rcfile : Stateid.t -> Stateid.t
val push_include : string -> Names.DirPath.t -> bool -> unit
(** [push_include phys_path log_path implicit] *)
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 2282932d4..4641a2bc8 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -7,11 +7,6 @@
(************************************************************************)
open Pp
-open CErrors
-open Util
-open Flags
-open Vernac
-open Pcoq
let top_stderr x =
Format.fprintf !Topfmt.err_ft "@[%a@]%!" pp_with x
@@ -24,7 +19,7 @@ type input_buffer = {
mutable str : Bytes.t; (* buffer of already read characters *)
mutable len : int; (* number of chars in the buffer *)
mutable bols : int list; (* offsets in str of beginning of lines *)
- mutable tokens : Gram.coq_parsable; (* stream of tokens *)
+ mutable tokens : Pcoq.Gram.coq_parsable; (* stream of tokens *)
mutable start : int } (* stream count of the first char of the buffer *)
(* Double the size of the buffer. *)
@@ -61,7 +56,7 @@ let prompt_char ic ibuf count =
| ll::_ -> Int.equal ibuf.len ll
| [] -> Int.equal ibuf.len 0
in
- if bol && not !print_emacs then top_stderr (str (ibuf.prompt()));
+ if bol && not !Flags.print_emacs then top_stderr (str (ibuf.prompt()));
try
let c = input_char ic in
if c == '\n' then ibuf.bols <- (ibuf.len+1) :: ibuf.bols;
@@ -78,7 +73,7 @@ let reset_input_buffer ic ibuf =
ibuf.str <- Bytes.empty;
ibuf.len <- 0;
ibuf.bols <- [];
- ibuf.tokens <- Gram.parsable (Stream.from (prompt_char ic ibuf));
+ ibuf.tokens <- Pcoq.Gram.parsable (Stream.from (prompt_char ic ibuf));
ibuf.start <- 0
(* Functions to print underlined locations from an input buffer. *)
@@ -89,7 +84,7 @@ module TopErr = struct
let get_bols_of_loc ibuf (bp,ep) =
let add_line (b,e) lines =
- if b < 0 || e < b then anomaly (Pp.str "Bad location");
+ if b < 0 || e < b then CErrors.anomaly (Pp.str "Bad location");
match lines with
| ([],None) -> ([], Some (b,e))
| (fl,oe) -> ((b,e)::fl, oe)
@@ -174,7 +169,7 @@ let error_info_for_buffer ?loc buf =
let fname = loc.Loc.fname in
let hl, loc =
(* We are in the toplevel *)
- if String.equal fname "" then
+ if CString.equal fname "" then
let nloc = adjust_loc_buf buf loc in
if valid_buffer_loc buf loc then
(fnl () ++ print_highlight_location buf nloc, nloc)
@@ -223,7 +218,7 @@ let make_emacs_prompt() =
let pending = Stm.get_all_proof_names() in
let pendingprompt =
List.fold_left
- (fun acc x -> acc ^ (if String.is_empty acc then "" else "|") ^ Names.Id.to_string x)
+ (fun acc x -> acc ^ (if CString.is_empty acc then "" else "|") ^ Names.Id.to_string x)
"" pending in
let proof_info = if dpth >= 0 then string_of_int dpth else "0" in
if !Flags.print_emacs then statnum ^ " |" ^ pendingprompt ^ "| " ^ proof_info ^ " < "
@@ -243,7 +238,7 @@ let top_buffer =
str = Bytes.empty;
len = 0;
bols = [];
- tokens = Gram.parsable (Stream.of_list []);
+ tokens = Pcoq.Gram.parsable (Stream.of_list []);
start = 0 }
let set_prompt prompt =
@@ -257,10 +252,10 @@ let set_prompt prompt =
let parse_to_dot =
let rec dot st = match Stream.next st with
| Tok.KEYWORD ("."|"...") -> ()
- | Tok.EOI -> raise End_of_input
+ | Tok.EOI -> raise Stm.End_of_input
| _ -> dot st
in
- Gram.Entry.of_parser "Coqtoplevel.dot" dot
+ Pcoq.Gram.Entry.of_parser "Coqtoplevel.dot" dot
(* If an error occurred while parsing, we try to read the input until a dot
token is encountered.
@@ -268,21 +263,19 @@ let parse_to_dot =
let rec discard_to_dot () =
try
- Gram.entry_parse parse_to_dot top_buffer.tokens
+ Pcoq.Gram.entry_parse parse_to_dot top_buffer.tokens
with
| Token.Error _ | CLexer.Error.E _ -> discard_to_dot ()
- | End_of_input -> raise End_of_input
+ | Stm.End_of_input -> raise Stm.End_of_input
| e when CErrors.noncritical e -> ()
-let read_sentence input =
- try
- let (loc, _ as r) = Vernac.parse_sentence input in
- CWarnings.set_current_loc loc; r
+let read_sentence sid input =
+ try Stm.parse_sentence sid input
with reraise ->
let reraise = CErrors.push reraise in
discard_to_dot ();
TopErr.print_toplevel_parse_error reraise top_buffer;
- iraise reraise
+ Exninfo.iraise reraise
(** Coqloop Console feedback handler *)
let coqloop_feed (fb : Feedback.feedback) = let open Feedback in
@@ -312,25 +305,24 @@ let coqloop_feed (fb : Feedback.feedback) = let open Feedback in
is caught and handled (i.e. not re-raised).
*)
-let do_vernac () =
+let do_vernac sid =
top_stderr (fnl());
- if !print_emacs then top_stderr (str (top_buffer.prompt()));
+ if !Flags.print_emacs then top_stderr (str (top_buffer.prompt()));
resynch_buffer top_buffer;
try
let input = (top_buffer.tokens, None) in
- Vernac.process_expr top_buffer.tokens (read_sentence input)
+ Vernac.process_expr sid top_buffer.tokens (read_sentence sid (fst input))
with
- | End_of_input | CErrors.Quit ->
+ | Stm.End_of_input | CErrors.Quit ->
top_stderr (fnl ()); raise CErrors.Quit
| CErrors.Drop -> (* Last chance *)
if Mltop.is_ocaml_top() then raise CErrors.Drop
- else Feedback.msg_error (str "There is no ML toplevel.")
+ else (Feedback.msg_error (str "There is no ML toplevel."); sid)
(* Exception printing is done now by the feedback listener. *)
(* XXX: We need this hack due to the side effects of the exception
printer and the reliance of Stm.define on attaching crutial
state to exceptions *)
- | any -> ignore (CErrors.(iprint (push any)))
-
+ | any -> ignore (CErrors.(iprint (push any))); sid
(** Main coq loop : read vernacular expressions until Drop is entered.
Ctrl-C is handled internally as Sys.Break instead of aborting Coq.
@@ -348,11 +340,16 @@ let loop_flush_all () =
let rec loop () =
Sys.catch_break true;
- if !Flags.print_emacs then Vernacentries.qed_display_script := false;
- Flags.coqtop_ui := true;
try
reset_input_buffer stdin top_buffer;
- while true do do_vernac(); loop_flush_all () done
+ (* Be careful to keep this loop tail-recursive *)
+ let rec vernac_loop sid =
+ let nsid = do_vernac sid in
+ loop_flush_all ();
+ vernac_loop nsid
+ (* We recover the current stateid, threading from the caller is
+ not possible due exceptions. *)
+ in vernac_loop (Stm.get_current_state ())
with
| CErrors.Drop -> ()
| CErrors.Quit -> exit 0
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index 8a34ded6d..66bbf43f6 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -31,7 +31,7 @@ val coqloop_feed : Feedback.feedback -> unit
(** Parse and execute one vernac command. *)
-val do_vernac : unit -> unit
+val do_vernac : Stateid.t -> Stateid.t
(** Main entry point of Coq: read and execute vernac commands. *)
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index aca94e63d..c259beb17 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -8,11 +8,8 @@
open Pp
open CErrors
-open Util
open Flags
-open Names
open Libnames
-open States
open Coqinit
let () = at_exit flush_all
@@ -133,10 +130,10 @@ let engage () =
let set_batch_mode () = batch_mode := true
-let toplevel_default_name = DirPath.make [Id.of_string "Top"]
+let toplevel_default_name = Names.(DirPath.make [Id.of_string "Top"])
let toplevel_name = ref toplevel_default_name
let set_toplevel_name dir =
- if DirPath.is_empty dir then error "Need a non empty toplevel module name";
+ if Names.DirPath.is_empty dir then error "Need a non empty toplevel module name";
toplevel_name := dir
let remove_top_ml () = Mltop.remove ()
@@ -150,9 +147,9 @@ let set_inputstate s =
warn_deprecated_inputstate ();
inputstate:=s
let inputstate () =
- if not (String.is_empty !inputstate) then
+ if not (CString.is_empty !inputstate) then
let fname = Loadpath.locate_file (CUnix.make_suffix !inputstate ".coq") in
- intern_state fname
+ States.intern_state fname
let warn_deprecated_outputstate =
CWarnings.create ~name:"deprecated-outputstate" ~category:"deprecated"
@@ -164,9 +161,9 @@ let set_outputstate s =
warn_deprecated_outputstate ();
outputstate:=s
let outputstate () =
- if not (String.is_empty !outputstate) then
+ if not (CString.is_empty !outputstate) then
let fname = CUnix.make_suffix !outputstate ".coq" in
- extern_state fname
+ States.extern_state fname
let set_include d p implicit =
let p = dirpath_of_string p in
@@ -175,15 +172,15 @@ let set_include d p implicit =
let load_vernacular_list = ref ([] : (string * bool) list)
let add_load_vernacular verb s =
load_vernacular_list := ((CUnix.make_suffix s ".v"),verb) :: !load_vernacular_list
-let load_vernacular () =
- List.iter
- (fun (s,b) ->
+let load_vernacular sid =
+ List.fold_left
+ (fun sid (s,v) ->
let s = Loadpath.locate_file s in
if !Flags.beautify then
- with_option beautify_file (Vernac.load_vernac b) s
+ with_option beautify_file (Vernac.load_vernac v sid) s
else
- Vernac.load_vernac b s)
- (List.rev !load_vernacular_list)
+ Vernac.load_vernac v sid s)
+ sid (List.rev !load_vernacular_list)
let load_vernacular_obj = ref ([] : string list)
let add_vernac_obj s = load_vernacular_obj := s :: !load_vernacular_obj
@@ -250,7 +247,6 @@ let set_emacs () =
if not (Option.is_empty !toploop) then
error "Flag -emacs is incompatible with a custom toplevel loop";
Flags.print_emacs := true;
- Vernacentries.qed_display_script := false;
color := `OFF
(** Options for CoqIDE *)
@@ -380,7 +376,7 @@ let get_host_port opt s =
let get_error_resilience opt = function
| "on" | "all" | "yes" -> `All
| "off" | "no" -> `None
- | s -> `Only (String.split ',' s)
+ | s -> `Only (CString.split ',' s)
let get_task_list s = List.map int_of_string (Str.split (Str.regexp ",") s)
@@ -625,7 +621,7 @@ let init_toplevel arglist =
init_load_path ();
Option.iter Mltop.load_ml_object_raw !toploop;
let extras = !toploop_init extras in
- if not (List.is_empty extras) then begin
+ if not (CList.is_empty extras) then begin
prerr_endline ("Don't know what to do with "^String.concat " " extras);
prerr_endline "See -help for the list of supported options";
exit 1
@@ -634,15 +630,16 @@ let init_toplevel arglist =
inputstate ();
Mltop.init_known_plugins ();
engage ();
- if (not !batch_mode || List.is_empty !compile_list)
+ if (not !batch_mode || CList.is_empty !compile_list)
&& Global.env_is_initial ()
then Declaremods.start_library !toplevel_name;
init_library_roots ();
load_vernac_obj ();
require ();
Stm.init ();
- load_rcfile();
- load_vernacular ();
+ let sid = load_rcfile (Stm.get_current_state ()) in
+ (* XXX: We ignore this for now, but should be threaded to the toplevels *)
+ let _sid = load_vernacular sid in
compile_files ();
schedule_vio_checking ();
schedule_vio_compilation ();
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 9917a49b4..98458a57a 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -13,111 +13,30 @@ open CErrors
open Util
open Flags
open Vernacexpr
+open Vernacprop
(* The functions in this module may raise (unexplainable!) exceptions.
Use the module Coqtoplevel, which catches these exceptions
(the exceptions are explained only at the toplevel). *)
-let user_error loc s = CErrors.user_err ~loc (str s)
-
-(* 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 checknav_simple loc cmd =
+let checknav_simple (loc, cmd) =
if is_navigation_vernac cmd && not (is_reset cmd) then
- user_error loc "Navigation commands forbidden in files."
+ CErrors.user_err ~loc (str "Navigation commands forbidden in files.")
-let checknav_deep loc ast =
+let checknav_deep (loc, ast) =
if is_deep_navigation_vernac ast then
- user_error loc "Navigation commands forbidden in nested commands."
-
-(* When doing Load on a file, two behaviors are possible:
-
- - either the history stack is grown by only one command,
- the "Load" itself. This is mandatory for command-counting
- interfaces (CoqIDE).
-
- - either each individual sub-commands in the file is added
- to the history stack. This allows commands like Show Script
- to work across the loaded file boundary (cf. bug #2820).
-
- The best of the two could probably be combined someday,
- in the meanwhile we use a flag. *)
-
-let atomic_load = ref true
-
-let _ =
- Goptions.declare_bool_option
- { Goptions.optsync = true;
- Goptions.optdepr = false;
- Goptions.optname = "atomic registration of commands in a Load";
- Goptions.optkey = ["Atomic";"Load"];
- Goptions.optread = (fun () -> !atomic_load);
- Goptions.optwrite = ((:=) atomic_load) }
+ CErrors.user_err ~loc (str "Navigation commands forbidden in nested commands.")
let disable_drop = function
| Drop -> CErrors.error "Drop is forbidden."
| e -> e
-(* Opening and closing a channel. Open it twice when verbose: the first
- channel is used to read the commands, and the second one to print them.
- Note: we could use only one thanks to seek_in, but seeking on and on in
- the file we parse seems a bit risky to me. B.B. *)
-
-let open_file_twice_if verbosely longfname =
- let in_chan = open_utf8_file_in longfname in
- let verb_ch =
- if verbosely then Some (open_utf8_file_in longfname) else None in
- let po = Pcoq.Gram.parsable ~file:longfname (Stream.of_channel in_chan) in
- (in_chan, longfname, (po, verb_ch))
-
-let close_input in_chan (_,verb) =
- try
- close_in in_chan;
- match verb with
- | Some verb_ch -> close_in verb_ch
- | _ -> ()
- with e when CErrors.noncritical e -> ()
-
-let verbose_phrase verbch loc =
- let loc = Loc.unloc loc in
- match verbch with
- | Some ch ->
- let len = snd loc - fst loc in
- let s = Bytes.create len in
- seek_in ch (fst loc);
- really_input ch s 0 len;
- Feedback.msg_notice (str (Bytes.to_string s))
- | None -> ()
-
-exception End_of_input
-
-let parse_sentence = Flags.with_option Flags.we_are_parsing
- (fun (po, verbch) ->
- match Pcoq.Gram.entry_parse Pcoq.main_entry po with
- | Some (loc,_ as com) -> verbose_phrase verbch loc; com
- | None -> raise End_of_input)
+(* Echo from a buffer based on position.
+ XXX: Should move to utility file. *)
+let vernac_echo loc in_chan = let open Loc in
+ let len = loc.ep - loc.bp in
+ seek_in in_chan loc.bp;
+ Feedback.msg_notice @@ str @@ really_input_string in_chan len
(* vernac parses the given stream, executes interpfun on the syntax tree it
* parses, and is verbose on "primitives" commands if verbosely is true *)
@@ -184,20 +103,43 @@ let print_cmd_header loc com =
Pp.pp_with !Topfmt.std_ft (pp_cmd_header loc com);
Format.pp_print_flush !Topfmt.std_ft ()
-let rec interp_vernac po chan_beautify checknav (loc,com) =
+let pr_open_cur_subgoals () =
+ try Printer.pr_open_subgoals ()
+ with Proof_global.NoCurrentProof -> Pp.str ""
+
+let rec interp_vernac sid po (loc,com) =
let interp = function
| VernacLoad (verbosely, fname) ->
let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in
let fname = CUnix.make_suffix fname ".v" in
let f = Loadpath.locate_file fname in
- load_vernac verbosely f
-
- | v -> Stm.interp (Flags.is_verbose()) (loc,v)
+ load_vernac verbosely sid f
+ | v ->
+ try
+ let nsid, ntip = Stm.add sid (Flags.is_verbose()) (loc,v) in
+
+ (* Main STM interaction *)
+ if ntip <> `NewTip then
+ anomaly (str "vernac.ml: We got an unfocus operation on the toplevel!");
+ (* Due to bug #5363 we cannot use observe here as we should,
+ it otherwise reveals bugs *)
+ (* Stm.observe nsid; *)
+ Stm.finish ();
+
+ (* We could use a more refined criteria depending on the
+ vernac. For now we imitate the old approach. *)
+ let print_goals = not (!Flags.batch_mode || is_query v) in
+
+ if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ());
+ nsid
+
+ with exn when CErrors.noncritical exn ->
+ ignore(Stm.edit_at sid);
+ raise exn
in
try
- checknav loc com;
- if !beautify then pr_new_syntax po chan_beautify loc (Some com);
- (* XXX: This is not 100% correct if called from an IDE context *)
+ (* The -time option is only supported from console-based
+ clients due to the way it prints. *)
if !Flags.time then print_cmd_header loc com;
let com = if !Flags.time then VernacTime (loc,com) else com in
interp com
@@ -208,26 +150,39 @@ let rec interp_vernac po chan_beautify checknav (loc,com) =
else iraise (reraise, info)
(* Load a vernac file. CErrors are annotated with file and location *)
-and load_vernac verbosely file =
+and load_vernac verbosely sid file =
let chan_beautify =
if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout in
- let (in_chan, fname, input) = open_file_twice_if verbosely file in
+ let in_chan = open_utf8_file_in file in
+ let in_echo = if verbosely then Some (open_utf8_file_in file) else None in
+ let in_pa = Pcoq.Gram.parsable ~file (Stream.of_channel in_chan) in
+ let rsid = ref sid in
try
(* we go out of the following infinite loop when a End_of_input is
* raised, which means that we raised the end of the file being loaded *)
while true do
- let loc_ast = Flags.silently parse_sentence input in
- CWarnings.set_current_loc (fst loc_ast);
- Flags.silently (interp_vernac (fst input) chan_beautify checknav_simple) loc_ast;
- done
+ let loc, ast = Stm.parse_sentence !rsid in_pa in
+
+ (* Printing of vernacs *)
+ if !beautify then pr_new_syntax in_pa chan_beautify loc (Some ast);
+ Option.iter (vernac_echo loc) in_echo;
+
+ checknav_simple (loc, ast);
+ let nsid = Flags.silently (interp_vernac !rsid in_pa) (loc, ast) in
+ rsid := nsid
+ done;
+ !rsid
with any -> (* whatever the exception *)
let (e, info) = CErrors.push any in
- close_input in_chan input; (* we must close the file first *)
+ close_in in_chan;
+ Option.iter close_in in_echo;
match e with
- | End_of_input ->
+ | Stm.End_of_input ->
+ (* Is this called so comments at EOF are printed? *)
if !beautify then
- pr_new_syntax (fst input) chan_beautify (Loc.make_loc (max_int,max_int)) None;
+ pr_new_syntax in_pa chan_beautify (Loc.make_loc (max_int,max_int)) None;
if !Flags.beautify_file then close_out chan_beautify;
+ !rsid
| reraise ->
if !Flags.beautify_file then close_out chan_beautify;
iraise (disable_drop e, info)
@@ -239,7 +194,9 @@ and load_vernac verbosely file =
of a new state label). An example of state-preserving command is one coming
from the query panel of Coqide. *)
-let process_expr po loc_ast = interp_vernac po stdout checknav_deep loc_ast
+let process_expr sid po loc_ast =
+ checknav_deep loc_ast;
+ interp_vernac sid po loc_ast
(* XML output hooks *)
let (f_xml_start_library, xml_start_library) = Hook.make ~default:ignore ()
@@ -308,7 +265,7 @@ let compile verbosely f =
Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n");
if !Flags.xml_export then Hook.get f_xml_start_library ();
let wall_clock1 = Unix.gettimeofday () in
- let _ = load_vernac verbosely long_f_dot_v in
+ let _ = load_vernac verbosely (Stm.get_current_state ()) long_f_dot_v in
Stm.join ();
let wall_clock2 = Unix.gettimeofday () in
check_pending_proofs ();
@@ -328,7 +285,7 @@ let compile verbosely f =
let ldir = Flags.verbosely Library.start_library long_f_dot_vio in
Dumpglob.noglob ();
Stm.set_compilation_hints long_f_dot_vio;
- let _ = load_vernac verbosely long_f_dot_v in
+ let _ = load_vernac verbosely (Stm.get_current_state ()) long_f_dot_v in
Stm.finish ();
check_pending_proofs ();
Stm.snapshot_vio ldir long_f_dot_vio;
@@ -347,6 +304,3 @@ let compile v f =
ignore(CoqworkmgrApi.get 1);
compile v f;
CoqworkmgrApi.giveback 1
-
-let () = Hook.set Stm.process_error_hook
- ExplainErr.process_vernac_interp_error
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index 0d9f5871a..e75f8f9e8 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -8,30 +8,16 @@
(** Parsing of vernacular. *)
-(** Read a vernac command on the specified input (parse only).
- Raises [End_of_file] if EOF (or Ctrl-D) is reached. *)
-
-val parse_sentence : Pcoq.Gram.coq_parsable * in_channel option ->
- Loc.t * Vernacexpr.vernac_expr
-
(** Reads and executes vernac commands from a stream. *)
+val process_expr : Stateid.t -> Pcoq.Gram.coq_parsable -> Vernacexpr.vernac_expr Loc.located -> Stateid.t
-exception End_of_input
+(** [load_vernac echo sid file] Loads [file] on top of [sid], will
+ echo the commands if [echo] is set. *)
+val load_vernac : bool -> Stateid.t -> string -> Stateid.t
-val process_expr : Pcoq.Gram.coq_parsable -> Loc.t * Vernacexpr.vernac_expr -> unit
+(** Compile a vernac file, (f is assumed without .v suffix) *)
+val compile : bool -> string -> unit
(** Set XML hooks *)
val xml_start_library : (unit -> unit) Hook.t
val xml_end_library : (unit -> unit) Hook.t
-
-(** Load a vernac file, verbosely or not. Errors are annotated with file
- and location *)
-
-val load_vernac : bool -> string -> unit
-
-
-(** Compile a vernac file, verbosely or not (f is assumed without .v suffix) *)
-
-val compile : bool -> string -> unit
-
-val is_navigation_vernac : Vernacexpr.vernac_expr -> bool
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 09:19:41 +0000