aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/base_include2
-rw-r--r--ide/coq.ml4
-rw-r--r--ide/coq.mli3
-rw-r--r--ide/coqide.ml2
-rw-r--r--ide/ide_slave.ml5
-rw-r--r--lib/flags.ml2
-rw-r--r--lib/flags.mli1
-rw-r--r--proofs/proof_global.ml1
-rw-r--r--proofs/proof_global.mli1
-rw-r--r--stm/proofworkertop.ml2
-rw-r--r--stm/queryworkertop.ml2
-rw-r--r--stm/stm.ml3
-rw-r--r--stm/tacworkertop.ml2
-rw-r--r--toplevel/coqinit.ml8
-rw-r--r--toplevel/coqinit.mli2
-rw-r--r--toplevel/coqloop.ml33
-rw-r--r--toplevel/coqloop.mli6
-rw-r--r--toplevel/coqtop.ml73
-rw-r--r--toplevel/coqtop.mli7
-rw-r--r--toplevel/vernac.ml43
-rw-r--r--toplevel/vernac.mli14
21 files changed, 124 insertions, 92 deletions
diff --git a/dev/base_include b/dev/base_include
index 320d366aa..350ccaa10 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -229,7 +229,7 @@ let _ = Flags.in_toplevel := true
let _ = Constrextern.set_extern_reference
(fun ?loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Id.Set.empty r));;
-let go () = Coqloop.loop Option.(get !Coqtop.drop_last_doc)
+let go () = Coqloop.loop ~time:false ~state:Option.(get !Coqtop.drop_last_doc)
let _ =
print_string
diff --git a/ide/coq.ml b/ide/coq.ml
index 42ab86dd6..34b4875af 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -9,6 +9,8 @@
open Ideutils
open Preferences
+let ideslave_coqtop_flags = ref None
+
(** * Version and date *)
let get_version_date () =
@@ -375,7 +377,7 @@ let spawn_handle args respawner feedback_processor =
in
let args = Array.of_list ("--xml_format=Ppcmds" :: "-async-proofs" :: async_default :: "-ideslave" :: args) in
let env =
- match !Flags.ideslave_coqtop_flags with
+ match !ideslave_coqtop_flags with
| None -> None
| Some s ->
let open Str in
diff --git a/ide/coq.mli b/ide/coq.mli
index 463dd134a..8c4727b37 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -171,3 +171,6 @@ val check_connection : string list -> unit
val interrupter : (int -> unit) ref
val save_all : (unit -> unit) ref
+
+(* Flags to be used for ideslave *)
+val ideslave_coqtop_flags : string option ref
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 3cc46b6aa..4de9a5288 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1360,7 +1360,7 @@ let read_coqide_args argv =
Backtrace.record_backtrace true;
filter_coqtop coqtop project_files ("-debug"::out) args
|"-coqtop-flags" :: flags :: args->
- Flags.ideslave_coqtop_flags := Some flags;
+ Coq.ideslave_coqtop_flags := Some flags;
filter_coqtop coqtop project_files out args
|arg::args when out = [] && Minilib.is_prefix_of "-psn_" arg ->
(* argument added by MacOS during .app launch *)
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 6d1064d25..fe86df084 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -458,8 +458,9 @@ let msg_format = ref (fun () ->
(* The loop ignores the command line arguments as the current model delegates
its handing to the toplevel container. *)
-let loop _args doc =
- set_doc doc;
+let loop _args ~state =
+ let open Vernac.State in
+ set_doc state.doc;
init_signal_handler ();
catch_break := false;
let in_ch, out_ch = Spawned.get_channels () in
diff --git a/lib/flags.ml b/lib/flags.ml
index 01361dad5..415e4399a 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -56,10 +56,8 @@ let in_toplevel = ref false
let profile = false
let ide_slave = ref false
-let ideslave_coqtop_flags = ref None
let raw_print = ref false
-
let univ_print = ref false
let we_are_parsing = ref false
diff --git a/lib/flags.mli b/lib/flags.mli
index 33d281798..c82410f07 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -33,7 +33,6 @@ val profile : bool
(* -ide_slave: printing will be more verbose, will affect stm caching *)
val ide_slave : bool ref
-val ideslave_coqtop_flags : string option ref
(* development flag to detect race conditions, it should go away. *)
val we_are_parsing : bool ref
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index fc94a1013..833e34c33 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -146,6 +146,7 @@ let cur_pstate () =
| [] -> raise NoCurrentProof
let give_me_the_proof () = (cur_pstate ()).proof
+let give_me_the_proof_opt () = try Some (give_me_the_proof ()) with | NoCurrentProof -> None
let get_current_proof_name () = (cur_pstate ()).pid
let with_current_proof f =
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 27e99f218..29445a746 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -24,6 +24,7 @@ val discard : Names.Id.t Loc.located -> unit
val discard_current : unit -> unit
val discard_all : unit -> unit
+val give_me_the_proof_opt : unit -> Proof.t option
exception NoCurrentProof
val give_me_the_proof : unit -> Proof.t
(** @raise NoCurrentProof when outside proof mode. *)
diff --git a/stm/proofworkertop.ml b/stm/proofworkertop.ml
index def60d1b9..81637f143 100644
--- a/stm/proofworkertop.ml
+++ b/stm/proofworkertop.ml
@@ -10,5 +10,5 @@ module W = AsyncTaskQueue.MakeWorker(Stm.ProofTask) ()
let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout
-let () = Coqtop.toploop_run := (fun _ _ -> W.main_loop ())
+let () = Coqtop.toploop_run := (fun _ ~state:_ -> W.main_loop ())
diff --git a/stm/queryworkertop.ml b/stm/queryworkertop.ml
index 928a6bfb0..7862f2f44 100644
--- a/stm/queryworkertop.ml
+++ b/stm/queryworkertop.ml
@@ -10,5 +10,5 @@ module W = AsyncTaskQueue.MakeWorker(Stm.QueryTask) ()
let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout
-let () = Coqtop.toploop_run := (fun _ _ -> W.main_loop ())
+let () = Coqtop.toploop_run := (fun _ ~state:_ -> W.main_loop ())
diff --git a/stm/stm.ml b/stm/stm.ml
index 6c956e134..92587b8ea 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2106,8 +2106,7 @@ and Reach : sig
end = struct (* {{{ *)
let async_policy () =
- let open Flags in
- if is_universe_polymorphism () then false
+ if Flags.is_universe_polymorphism () then false
else if VCS.is_interactive () = `Yes then
(async_proofs_is_master !cur_opt || !cur_opt.async_proofs_mode = APonLazy)
else
diff --git a/stm/tacworkertop.ml b/stm/tacworkertop.ml
index f202fc7c5..22b45a9be 100644
--- a/stm/tacworkertop.ml
+++ b/stm/tacworkertop.ml
@@ -10,5 +10,5 @@ module W = AsyncTaskQueue.MakeWorker(Stm.TacTask) ()
let () = Coqtop.toploop_init := WorkerLoop.loop W.init_stdout
-let () = Coqtop.toploop_run := (fun _ _ -> W.main_loop ())
+let () = Coqtop.toploop_run := (fun _ ~state:_ -> W.main_loop ())
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 8574092b8..d8aaf3db8 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -21,12 +21,12 @@ let set_debug () =
let rcdefaultname = "coqrc"
-let load_rcfile ~rcfile ~time doc sid =
+let load_rcfile ~rcfile ~time ~state =
try
match rcfile with
| Some rcfile ->
if CUnix.file_readable_p rcfile then
- Vernac.load_vernac ~time ~verbosely:false ~interactive:false ~check:true doc sid rcfile
+ Vernac.load_vernac ~time ~verbosely:false ~interactive:false ~check:true ~state rcfile
else raise (Sys_error ("Cannot read rcfile: "^ rcfile))
| None ->
try
@@ -37,8 +37,8 @@ let load_rcfile ~rcfile ~time doc sid =
Envars.home ~warn / "."^rcdefaultname^"."^Coq_config.version;
Envars.home ~warn / "."^rcdefaultname
] in
- Vernac.load_vernac ~time ~verbosely:false ~interactive:false ~check:true doc sid inferedrc
- with Not_found -> doc, sid
+ Vernac.load_vernac ~time ~verbosely:false ~interactive:false ~check:true ~state inferedrc
+ with Not_found -> state
(*
Flags.if_verbose
mSGNL (str ("No coqrc or coqrc."^Coq_config.version^
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index 0ceba5b38..14f39170c 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -10,7 +10,7 @@
val set_debug : unit -> unit
-val load_rcfile : rcfile:(string option) -> time:bool -> Stm.doc -> Stateid.t -> Stm.doc * Stateid.t
+val load_rcfile : rcfile:(string option) -> time:bool -> state:Vernac.State.t -> Vernac.State.t
val init_ocaml_path : unit -> unit
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index aade101a4..ae0b94476 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -258,8 +258,9 @@ let rec discard_to_dot () =
| Stm.End_of_input -> raise Stm.End_of_input
| e when CErrors.noncritical e -> ()
-let read_sentence ~doc sid input =
- try Stm.parse_sentence ~doc sid input
+let read_sentence ~state input =
+ let open Vernac.State in
+ try Stm.parse_sentence ~doc:state.doc state.sid input
with reraise ->
let reraise = CErrors.push reraise in
discard_to_dot ();
@@ -300,19 +301,20 @@ let coqloop_feed (fb : Feedback.feedback) = let open Feedback in
is caught and handled (i.e. not re-raised).
*)
-let do_vernac ~time doc sid =
+let do_vernac ~time ~state =
+ let open Vernac.State in
top_stderr (fnl());
- if !print_emacs then top_stderr (str (top_buffer.prompt doc));
+ if !print_emacs then top_stderr (str (top_buffer.prompt state.doc));
resynch_buffer top_buffer;
try
let input = (top_buffer.tokens, None) in
- Vernac.process_expr ~time doc sid (read_sentence ~doc sid (fst input))
+ Vernac.process_expr ~time ~state (read_sentence ~state (fst input))
with
| 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_warning (str "There is no ML toplevel."); doc, sid)
+ else (Feedback.msg_warning (str "There is no ML toplevel."); state)
(* Exception printing should be done by the feedback listener,
however this is not yet ready so we rely on the exception for
now. *)
@@ -321,7 +323,7 @@ let do_vernac ~time doc sid =
let loc = Loc.get_loc info in
let msg = CErrors.iprint (e, info) in
TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer;
- doc, sid
+ state
(** Main coq loop : read vernacular expressions until Drop is entered.
Ctrl-C is handled internally as Sys.Break instead of aborting Coq.
@@ -337,20 +339,21 @@ let loop_flush_all () =
Format.pp_print_flush !Topfmt.std_ft ();
Format.pp_print_flush !Topfmt.err_ft ()
-let rec loop ~time doc =
+let rec loop ~time ~state =
+ let open Vernac.State in
Sys.catch_break true;
try
- reset_input_buffer doc stdin top_buffer;
+ reset_input_buffer state.doc stdin top_buffer;
(* Be careful to keep this loop tail-recursive *)
- let rec vernac_loop doc sid =
- let ndoc, nsid = do_vernac ~time doc sid in
+ let rec vernac_loop ~state =
+ let nstate = do_vernac ~time ~state in
loop_flush_all ();
- vernac_loop ndoc nsid
+ vernac_loop ~state:nstate
(* We recover the current stateid, threading from the caller is
not possible due exceptions. *)
- in vernac_loop doc (Stm.get_current_state ~doc)
+ in vernac_loop ~state
with
- | CErrors.Drop -> doc
+ | CErrors.Drop -> state
| CErrors.Quit -> exit 0
| any ->
top_stderr (str "Anomaly: main loop exited with exception: " ++
@@ -358,4 +361,4 @@ let rec loop ~time doc =
fnl() ++
str"Please report" ++
strbrk" at " ++ str Coq_config.wwwbugtracker ++ str ".");
- loop ~time doc
+ loop ~time ~state
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index 09240ec82..1c1309051 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -31,9 +31,7 @@ val set_prompt : (unit -> string) -> unit
val coqloop_feed : Feedback.feedback -> unit
(** Parse and execute one vernac command. *)
-
-val do_vernac : time:bool -> Stm.doc -> Stateid.t -> Stm.doc * Stateid.t
+val do_vernac : time:bool -> state:Vernac.State.t -> Vernac.State.t
(** Main entry point of Coq: read and execute vernac commands. *)
-
-val loop : time:bool -> Stm.doc -> Stm.doc
+val loop : time:bool -> state:Vernac.State.t -> Vernac.State.t
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 9058f0846..26ede1834 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -37,16 +37,16 @@ let coqtop_init_feed = Coqloop.coqloop_feed
let drop_last_doc = ref None
(* Default toplevel loop *)
-let console_toploop_run opts doc =
+let console_toploop_run opts ~state =
(* We initialize the console only if we run the toploop_run *)
let tl_feed = Feedback.add_feeder Coqloop.coqloop_feed in
if Dumpglob.dump () then begin
Flags.if_verbose warning "Dumpglob cannot be used in interactive mode.";
Dumpglob.noglob ()
end;
- let doc = Coqloop.loop ~time:opts.time doc in
+ let state = Coqloop.loop ~time:opts.time ~state in
(* Initialise and launch the Ocaml toplevel *)
- drop_last_doc := Some doc;
+ drop_last_doc := Some state;
Coqinit.init_ocaml_path();
Mltop.ocaml_toploop();
(* We let the feeder in place for users of Drop *)
@@ -90,24 +90,26 @@ let outputstate opts =
(******************************************************************************)
(* Interactive Load File Simulation *)
(******************************************************************************)
-let load_vernacular opts doc sid =
+let load_vernacular opts ~state =
List.fold_left
- (fun (doc,sid) (f_in, verbosely) ->
+ (fun state (f_in, verbosely) ->
let s = Loadpath.locate_file f_in in
- if !Flags.beautify then
- Flags.with_option Flags.beautify_file (Vernac.load_vernac ~time:opts.time ~verbosely ~interactive:false ~check:true doc sid) f_in
- else
- Vernac.load_vernac ~time:opts.time ~verbosely ~interactive:false ~check:true doc sid s)
- (doc, sid) (List.rev opts.load_vernacular_list)
-
-let load_init_vernaculars opts doc sid =
- let doc, sid = if opts.load_rcfile then
- Coqinit.load_rcfile ~rcfile:opts.rcfile ~time:opts.time doc sid
+ (* Should make the beautify logic clearer *)
+ let load_vernac f = Vernac.load_vernac ~time:opts.time ~verbosely ~interactive:false ~check:true ~state f in
+ if !Flags.beautify
+ then Flags.with_option Flags.beautify_file load_vernac f_in
+ else load_vernac s
+ ) state (List.rev opts.load_vernacular_list)
+
+let load_init_vernaculars opts ~state =
+ let state = if opts.load_rcfile then
+ Coqinit.load_rcfile ~rcfile:opts.rcfile ~time:opts.time ~state
else begin
Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading.");
- doc,sid
+ state
end in
- load_vernacular opts doc sid
+
+ load_vernacular opts ~state
(******************************************************************************)
(* Startup LoadPath and Modules *)
@@ -193,6 +195,7 @@ let ensure_exists f =
(* Compile a vernac file *)
let compile opts ~verbosely ~f_in ~f_out =
+ let open Vernac.State in
let check_pending_proofs () =
let pfs = Proof_global.get_all_proof_names () in
if not (CList.is_empty pfs) then
@@ -220,16 +223,17 @@ let compile opts ~verbosely ~f_in ~f_out =
iload_path; require_libs; stm_options;
}) in
- let doc, sid = load_init_vernaculars opts doc sid in
- let ldir = Stm.get_ldir ~doc in
+ let state = { doc; sid; proof = None } in
+ let state = load_init_vernaculars opts ~state in
+ let ldir = Stm.get_ldir ~doc:state.doc in
Aux_file.(start_aux_file
~aux_file:(aux_file_name_for long_f_dot_vo)
~v_file:long_f_dot_v);
Dumpglob.start_dump_glob ~vfile:long_f_dot_v ~vofile:long_f_dot_vo;
Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n");
let wall_clock1 = Unix.gettimeofday () in
- let doc, _ = Vernac.load_vernac ~time:opts.time ~verbosely ~check:true ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in
- let _doc = Stm.join ~doc in
+ let state = Vernac.load_vernac ~time:opts.time ~verbosely ~check:true ~interactive:false ~state long_f_dot_v in
+ let _doc = Stm.join ~doc:state.doc in
let wall_clock2 = Unix.gettimeofday () in
check_pending_proofs ();
Library.save_library_to ldir long_f_dot_vo (Global.opaque_tables ());
@@ -266,11 +270,11 @@ let compile opts ~verbosely ~f_in ~f_out =
iload_path; require_libs; stm_options;
}) in
- let doc, sid = load_init_vernaculars opts doc sid in
-
- let ldir = Stm.get_ldir ~doc in
- let doc, _ = Vernac.load_vernac ~time:opts.time ~verbosely ~check:false ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in
- let doc = Stm.finish ~doc in
+ let state = { doc; sid; proof = None } in
+ let state = load_init_vernaculars opts ~state in
+ let ldir = Stm.get_ldir ~doc:state.doc in
+ let state = Vernac.load_vernac ~time:opts.time ~verbosely ~check:false ~interactive:false ~state long_f_dot_v in
+ let doc = Stm.finish ~doc:state.doc in
check_pending_proofs ();
let _doc = Stm.snapshot_vio ~doc ldir long_f_dot_vio in
Stm.reset_task_queue ()
@@ -465,12 +469,15 @@ let init_toplevel arglist =
let iload_path = build_load_path opts in
let require_libs = require_libs opts in
let stm_options = opts.stm_flags in
- try let doc, sid =
- Stm.(new_doc
- { doc_type = Interactive opts.toplevel_name;
- iload_path; require_libs; stm_options;
- }) in
- Some (load_init_vernaculars opts doc sid), opts
+ try
+ let open Vernac.State in
+ let doc, sid =
+ Stm.(new_doc
+ { doc_type = Interactive opts.toplevel_name;
+ iload_path; require_libs; stm_options;
+ }) in
+ let state = { doc; sid; proof = None } in
+ Some (load_init_vernaculars opts ~state), opts
with any -> flush_all(); fatal_error_exn any
(* Non interactive: we perform a sequence of compilation steps *)
end else begin
@@ -496,8 +503,8 @@ let init_toplevel arglist =
let start () =
match init_toplevel (List.tl (Array.to_list Sys.argv)) with
(* Batch mode *)
- | Some (doc, sid), opts when not opts.batch_mode ->
- !toploop_run opts doc;
+ | Some state, opts when not opts.batch_mode ->
+ !toploop_run opts ~state;
exit 1
| _ , opts ->
flush_all();
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index 4d625a03d..dedb298e2 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -11,14 +11,13 @@
state, load the files given on the command line, load the resource file,
produce the output state if any, and finally will launch [Coqloop.loop]. *)
-val init_toplevel : string list -> (Stm.doc * Stateid.t) option * Coqargs.coq_cmdopts
+val init_toplevel : string list -> Vernac.State.t option * Coqargs.coq_cmdopts
val start : unit -> unit
(* Last document seen after `Drop` *)
-val drop_last_doc : Stm.doc option ref
+val drop_last_doc : Vernac.State.t option ref
(* For other toploops *)
val toploop_init : (Coqargs.coq_cmdopts -> string list -> string list) ref
-val toploop_run : (Coqargs.coq_cmdopts -> Stm.doc -> unit) ref
-
+val toploop_run : (Coqargs.coq_cmdopts -> state:Vernac.State.t -> unit) ref
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 6b45a94bc..1f681d9cf 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -110,14 +110,25 @@ let pr_open_cur_subgoals () =
(* Stm.End_of_input -> true *)
(* | _ -> false *)
-let rec interp_vernac ~time ~check ~interactive doc sid (loc,com) =
+module State = struct
+
+ type t = {
+ doc : Stm.doc;
+ sid : Stateid.t;
+ proof : Proof.t option;
+ }
+
+end
+
+let rec interp_vernac ~time ~check ~interactive ~state (loc,com) =
+ let open State in
let interp v =
match under_control v with
| 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 ~time ~verbosely ~check ~interactive doc sid f
+ load_vernac ~time ~verbosely ~check ~interactive ~state f
| _ ->
(* XXX: We need to run this before add as the classification is
highly dynamic and depends on the structure of the
@@ -134,7 +145,7 @@ let rec interp_vernac ~time ~check ~interactive doc sid (loc,com) =
in
CWarnings.set_flags wflags;
- let doc, nsid, ntip = Stm.add ~doc ~ontop:sid (not !Flags.quiet) (loc,v) in
+ let doc, nsid, ntip = Stm.add ~doc:state.doc ~ontop:state.sid (not !Flags.quiet) (loc,v) in
(* Main STM interaction *)
if ntip <> `NewTip then
@@ -152,7 +163,8 @@ let rec interp_vernac ~time ~check ~interactive doc sid (loc,com) =
is_proof_step && Proof_global.there_are_pending_proofs () in
if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ());
- ndoc, nsid
+ let new_proof = Proof_global.give_me_the_proof_opt () in
+ { doc = ndoc; sid = nsid; proof = new_proof }
in
try
(* The -time option is only supported from console-based
@@ -163,7 +175,7 @@ let rec interp_vernac ~time ~check ~interactive doc sid (loc,com) =
with reraise ->
(* XXX: In non-interactive mode edit_at seems to do very weird
things, so we better avoid it while we investigate *)
- if interactive then ignore(Stm.edit_at ~doc sid);
+ if interactive then ignore(Stm.edit_at ~doc:state.doc state.sid);
let (reraise, info) = CErrors.push reraise in
let info = begin
match Loc.get_loc info with
@@ -172,7 +184,7 @@ let rec interp_vernac ~time ~check ~interactive doc sid (loc,com) =
end in iraise (reraise, info)
(* Load a vernac file. CErrors are annotated with file and location *)
-and load_vernac ~time ~verbosely ~check ~interactive doc sid file =
+and load_vernac ~time ~verbosely ~check ~interactive ~state file =
let ft_beautify, close_beautify =
if !Flags.beautify_file then
let chan_beautify = open_out (file^beautify_suffix) in
@@ -183,14 +195,14 @@ and load_vernac ~time ~verbosely ~check ~interactive doc sid file =
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:(Loc.InFile file) (Stream.of_channel in_chan) in
- let rsid = ref sid in
- let rdoc = ref doc in
+ let rstate = ref state in
+ let open State 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 =
- Stm.parse_sentence ~doc:!rdoc !rsid in_pa
+ Stm.parse_sentence ~doc:!rstate.doc !rstate.sid in_pa
(* If an error in parsing occurs, we propagate the exception
so the caller of load_vernac will take care of it. However,
in the future it could be possible that we want to handle
@@ -214,11 +226,10 @@ and load_vernac ~time ~verbosely ~check ~interactive doc sid file =
Option.iter (vernac_echo ?loc) in_echo;
checknav_simple (loc, ast);
- let ndoc, nsid = Flags.silently (interp_vernac ~time ~check ~interactive !rdoc !rsid) (loc, ast) in
- rsid := nsid;
- rdoc := ndoc
+ let state = Flags.silently (interp_vernac ~time ~check ~interactive ~state:!rstate) (loc, ast) in
+ rstate := state;
done;
- !rdoc, !rsid
+ !rstate
with any -> (* whatever the exception *)
let (e, info) = CErrors.push any in
close_in in_chan;
@@ -229,7 +240,7 @@ and load_vernac ~time ~verbosely ~check ~interactive doc sid file =
if !Flags.beautify then
pr_new_syntax ~loc:(Loc.make_loc (max_int,max_int)) in_pa ft_beautify None;
if !Flags.beautify_file then close_beautify ();
- !rdoc, !rsid
+ !rstate
| reraise ->
if !Flags.beautify_file then close_beautify ();
iraise (disable_drop e, info)
@@ -241,6 +252,6 @@ and load_vernac ~time ~verbosely ~check ~interactive doc sid file =
of a new state label). An example of state-preserving command is one coming
from the query panel of Coqide. *)
-let process_expr ~time doc sid loc_ast =
+let process_expr ~time ~state loc_ast =
checknav_deep loc_ast;
- interp_vernac ~time ~interactive:true ~check:true doc sid loc_ast
+ interp_vernac ~time ~interactive:true ~check:true ~state loc_ast
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index b77b024fa..e909ada1e 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -7,14 +7,24 @@
(************************************************************************)
(** Parsing of vernacular. *)
+module State : sig
+
+ type t = {
+ doc : Stm.doc;
+ sid : Stateid.t;
+ proof : Proof.t option;
+ }
+
+end
(** [process_expr sid cmd] Executes vernac command [cmd]. Callers are
expected to handle and print errors in form of exceptions, however
care is taken so the state machine is left in a consistent
state. *)
-val process_expr : time:bool -> Stm.doc -> Stateid.t -> Vernacexpr.vernac_control Loc.located -> Stm.doc * Stateid.t
+val process_expr : time:bool -> state:State.t -> Vernacexpr.vernac_control Loc.located -> State.t
(** [load_vernac echo sid file] Loads [file] on top of [sid], will
echo the commands if [echo] is set. Callers are expected to handle
and print errors in form of exceptions. *)
-val load_vernac : time:bool -> verbosely:bool -> check:bool -> interactive:bool -> Stm.doc -> Stateid.t -> string -> Stm.doc * Stateid.t
+val load_vernac : time:bool -> verbosely:bool -> check:bool -> interactive:bool ->
+ state:State.t -> string -> State.t
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 12:57:04 +0000