aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/base_include2
-rw-r--r--ide/ide_slave.ml2
-rw-r--r--intf/vernacexpr.ml2
-rw-r--r--lib/cErrors.ml4
-rw-r--r--lib/cErrors.mli2
-rw-r--r--parsing/g_vernac.ml44
-rw-r--r--printing/ppvernac.ml6
-rw-r--r--stm/stm.ml6
-rw-r--r--stm/vernac_classifier.ml1
-rw-r--r--toplevel/coqinit.ml6
-rw-r--r--toplevel/coqinit.mli4
-rw-r--r--toplevel/coqloop.ml106
-rw-r--r--toplevel/coqloop.mli5
-rw-r--r--toplevel/coqtop.ml16
-rw-r--r--toplevel/g_toplevel.ml443
-rw-r--r--toplevel/toplevel.mllib1
-rw-r--r--toplevel/vernac.ml30
-rw-r--r--toplevel/vernac.mli5
-rw-r--r--vernac/vernacentries.ml3
-rw-r--r--vernac/vernacinterp.ml1
20 files changed, 123 insertions, 126 deletions
diff --git a/dev/base_include b/dev/base_include
index 1fb80dc07..e76044f41 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -232,7 +232,7 @@ let _ = Flags.in_toplevel := true
let _ = Constrextern.set_extern_reference
(fun ?loc _ r -> CAst.make ?loc @@ Libnames.Qualid (Nametab.shortest_qualid_of_global Id.Set.empty r));;
-let go () = Coqloop.loop ~time:false ~state:Option.(get !Coqloop.drop_last_doc)
+let go () = Coqloop.loop ~state:Option.(get !Coqloop.drop_last_doc)
let _ =
print_string
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 6b7efc839..2e552b60b 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -359,8 +359,6 @@ let handle_exn (e, info) =
| _ -> None in
let mk_msg () = CErrors.print ~info e in
match e with
- | CErrors.Drop -> dummy, None, Pp.str "Drop is not allowed by coqide!"
- | CErrors.Quit -> dummy, None, Pp.str "Quit is not allowed by coqide!"
| e ->
match Stateid.get info with
| Some (valid, _) -> valid, loc_of info, mk_msg ()
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index df061bfb7..dc1110ad8 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -457,8 +457,6 @@ type nonrec vernac_expr =
| VernacCheckGuard
| VernacProof of Genarg.raw_generic_argument option * section_subset_expr option
| VernacProofMode of string
- (* Toplevel control *)
- | VernacToplevelControl of exn
(* For extension *)
| VernacExtend of extend_name * Genarg.raw_generic_argument list
diff --git a/lib/cErrors.ml b/lib/cErrors.ml
index 975022114..811fcf406 100644
--- a/lib/cErrors.ml
+++ b/lib/cErrors.ml
@@ -47,8 +47,6 @@ exception AlreadyDeclared of Pp.t (* for already declared Schemes *)
let alreadydeclared pps = raise (AlreadyDeclared(pps))
exception Timeout
-exception Drop
-exception Quit
let handle_stack = ref []
@@ -126,7 +124,7 @@ end
let noncritical = function
| Sys.Break | Out_of_memory | Stack_overflow
| Assert_failure _ | Match_failure _ | Anomaly _
- | Timeout | Drop | Quit -> false
+ | Timeout -> false
| Invalid_argument "equal: functional value" -> false
| _ -> true
[@@@ocaml.warning "+52"]
diff --git a/lib/cErrors.mli b/lib/cErrors.mli
index ec34dd62c..4e2fe7621 100644
--- a/lib/cErrors.mli
+++ b/lib/cErrors.mli
@@ -53,8 +53,6 @@ val invalid_arg : ?loc:Loc.t -> string -> 'a
val todo : string -> unit
exception Timeout
-exception Drop
-exception Quit
(** [register_handler h] registers [h] as a handler.
When an expression is printed with [print e], it
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 72c3cc14a..8543d2b84 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -845,10 +845,6 @@ GEXTEND Gram
| IDENT "Cd" -> VernacChdir None
| IDENT "Cd"; dir = ne_string -> VernacChdir (Some dir)
- (* Toplevel control *)
- | IDENT "Drop" -> VernacToplevelControl Drop
- | IDENT "Quit" -> VernacToplevelControl Quit
-
| IDENT "Load"; verbosely = [ IDENT "Verbose" -> true | -> false ];
s = [ s = ne_string -> s | s = IDENT -> s ] ->
VernacLoad (verbosely, s)
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 5c5b7206a..7df0a0c94 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -181,8 +181,6 @@ open Decl_kinds
| BoolValue b -> mt()
in pr_printoption a None ++ pr_opt_value b
- let pr_topcmd _ = str"(* <Warning> : No printer for toplevel commands *)"
-
let pr_opt_hintbases l = match l with
| [] -> mt()
| _ as z -> str":" ++ spc() ++ prlist_with_sep sep str z
@@ -1188,10 +1186,6 @@ open Decl_kinds
++ prlist_with_sep sep (pr_comment pr_constr) l)
)
- (* Toplevel control *)
- | VernacToplevelControl exn ->
- return (pr_topcmd exn)
-
(* For extension *)
| VernacExtend (s,c) ->
return (pr_extend s c)
diff --git a/stm/stm.ml b/stm/stm.ml
index ad94b6807..756b93c61 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2734,7 +2734,6 @@ let merge_proof_branch ~valid ?id qast keep brname =
(* 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 =
- if e = CErrors.Drop then Exninfo.iraise (e, info) else
match Stateid.get info with
| None ->
VCS.restore vcs;
@@ -2881,11 +2880,6 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true)
rc
(* Side effect on all branches *)
- | VtUnknown, _ when Vernacprop.under_control expr = VernacToplevelControl Drop ->
- let st = Vernacstate.freeze_interp_state `No in
- ignore(stm_vernac_interp (VCS.get_branch_pos head) st x);
- `Ok
-
| VtSideff l, w ->
let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in
let id = VCS.new_node ~id:newtip () in
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index f68c8b326..9a8af3a58 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -185,7 +185,6 @@ let classify_vernac e =
| VernacResetName _ | VernacResetInitial
| VernacBacktrack _ | VernacBackTo _ | VernacRestart -> VtMeta, VtNow
(* What are these? *)
- | VernacToplevelControl _
| VernacRestoreState _
| VernacWriteState _ -> VtSideff [], VtNow
(* Plugins should classify their commands *)
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 96a0bd5ec..3e7a83085 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -23,12 +23,12 @@ let set_debug () =
let rcdefaultname = "coqrc"
-let load_rcfile ~rcfile ~time ~state =
+let load_rcfile ~rcfile ~state =
try
match rcfile with
| Some rcfile ->
if CUnix.file_readable_p rcfile then
- Vernac.load_vernac ~time ~echo:false ~interactive:false ~check:true ~state rcfile
+ Vernac.load_vernac ~echo:false ~interactive:false ~check:true ~state rcfile
else raise (Sys_error ("Cannot read rcfile: "^ rcfile))
| None ->
try
@@ -39,7 +39,7 @@ let load_rcfile ~rcfile ~time ~state =
Envars.home ~warn / "."^rcdefaultname^"."^Coq_config.version;
Envars.home ~warn / "."^rcdefaultname
] in
- Vernac.load_vernac ~time ~echo:false ~interactive:false ~check:true ~state inferedrc
+ Vernac.load_vernac ~echo:false ~interactive:false ~check:true ~state inferedrc
with Not_found -> state
(*
Flags.if_verbose
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index 71b5523cd..c891e736b 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -12,12 +12,12 @@
val set_debug : unit -> unit
-val load_rcfile : rcfile:(string option) -> time:bool -> state:Vernac.State.t -> Vernac.State.t
+val load_rcfile : rcfile:(string option) -> state:Vernac.State.t -> Vernac.State.t
val init_ocaml_path : unit -> unit
(* LoadPath for toploop toplevels *)
-val toplevel_init_load_path : unit -> Mltop.coq_path list
+val toplevel_init_load_path : unit -> Mltop.coq_path list
(* LoadPath for Coq user libraries *)
val libs_init_load_path : load_init:bool -> Mltop.coq_path list
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index a103cfe7f..64d839f18 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -261,8 +261,8 @@ let rec discard_to_dot () =
| e when CErrors.noncritical e -> ()
let read_sentence ~state input =
- let open Vernac.State in
- try Stm.parse_sentence ~doc:state.doc state.sid input
+ (* XXX: careful with ignoring the state Eugene!*)
+ try G_toplevel.parse_toplevel input
with reraise ->
let reraise = CErrors.push reraise in
discard_to_dot ();
@@ -293,40 +293,6 @@ let coqloop_feed (fb : Feedback.feedback) = let open Feedback in
| Message (lvl,loc,msg) ->
TopErr.print_error_for_buffer ?loc lvl msg top_buffer
-(** [do_vernac] reads and executes a toplevel phrase, and print error
- messages when an exception is raised, except for the following:
- - Drop: kill the Coq toplevel, going down to the Caml toplevel if it exists.
- Otherwise, exit.
- - End_of_input: Ctrl-D was typed in, we will quit.
-
- In particular, this is normally the only place where a Sys.Break
- is caught and handled (i.e. not re-raised).
-*)
-
-let do_vernac ~time ~state =
- let open Vernac.State in
- top_stderr (fnl());
- 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 ~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."); state)
- (* Exception printing should be done by the feedback listener,
- however this is not yet ready so we rely on the exception for
- now. *)
- | any ->
- let (e, info) = CErrors.push any in
- 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;
- state
-
(** Main coq loop : read vernacular expressions until Drop is entered.
Ctrl-C is handled internally as Sys.Break instead of aborting Coq.
Normally, the only exceptions that can come out of [do_vernac] and
@@ -359,37 +325,55 @@ let cproof p1 p2 =
let drop_last_doc = ref None
-let rec loop ~time ~state =
+(* Careful to keep this loop tail-rec *)
+let rec vernac_loop ~state =
+ let open CAst in
let open Vernac.State in
- Sys.catch_break true;
+ let open G_toplevel in
+ loop_flush_all ();
+ top_stderr (fnl());
+ if !print_emacs then top_stderr (str (top_buffer.prompt state.doc));
+ resynch_buffer top_buffer;
+ (* execute one command *)
try
- reset_input_buffer state.doc stdin top_buffer;
- (* Be careful to keep this loop tail-recursive *)
- let rec vernac_loop ~state =
- let nstate = do_vernac ~time ~state in
+ let input = top_buffer.tokens in
+ match read_sentence ~state input with
+ | {v=VernacQuit} ->
+ exit 0
+ | {v=VernacDrop} ->
+ if Mltop.is_ocaml_top()
+ then (drop_last_doc := Some state; state)
+ else (Feedback.msg_warning (str "There is no ML toplevel."); vernac_loop ~state)
+ | {v=VernacControl c; loc} ->
+ let nstate = Vernac.process_expr ~state (make ?loc c) in
let proof_changed = not (Option.equal cproof nstate.proof state.proof) in
let print_goals = not !Flags.quiet &&
proof_changed && Proof_global.there_are_pending_proofs () in
if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ());
- loop_flush_all ();
vernac_loop ~state:nstate
- (* We recover the current stateid, threading from the caller is
- not possible due exceptions. *)
- in vernac_loop ~state
with
- | CErrors.Drop ->
- (* Due to using exceptions as a form of control, state here goes
- out of sync as [do_vernac] will never return. We must thus do
- this hack until we make `Drop` a toplevel-only command. See
- bug #6872. *)
- let state = { state with sid = Stm.get_current_state ~doc:state.doc } in
- drop_last_doc := Some state;
- state
- | CErrors.Quit -> exit 0
+ | Stm.End_of_input ->
+ top_stderr (fnl ()); exit 0
+ (* Exception printing should be done by the feedback listener,
+ however this is not yet ready so we rely on the exception for
+ now. *)
+ | any ->
+ let (e, info) = CErrors.push any in
+ 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;
+ vernac_loop ~state
+
+let rec loop ~state =
+ let open Vernac.State in
+ Sys.catch_break true;
+ try
+ reset_input_buffer state.doc stdin top_buffer;
+ vernac_loop ~state
+ with
| any ->
- top_stderr (str "Anomaly: main loop exited with exception: " ++
- str (Printexc.to_string any) ++
- fnl() ++
- str"Please report" ++
- strbrk" at " ++ str Coq_config.wwwbugtracker ++ str ".");
- loop ~time ~state
+ top_stderr
+ (hov 0 (str "Anomaly: main loop exited with exception:" ++ spc () ++
+ str (Printexc.to_string any)) ++ spc () ++
+ hov 0 (str "Please report at " ++ str Coq_config.wwwbugtracker ++ str "."));
+ loop ~state
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index bbb9b1383..39a9de4f8 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -32,11 +32,8 @@ val set_prompt : (unit -> string) -> unit
(** Toplevel feedback printer. *)
val coqloop_feed : Feedback.feedback -> unit
-(** Parse and execute one vernac command. *)
-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 -> state:Vernac.State.t -> Vernac.State.t
+val loop : state:Vernac.State.t -> Vernac.State.t
(** Last document seen after `Drop` *)
val drop_last_doc : Vernac.State.t option ref
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index cd831c05c..a08cfa9f4 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -45,7 +45,7 @@ let console_toploop_run opts ~state =
Flags.if_verbose warning "Dumpglob cannot be used in interactive mode.";
Dumpglob.noglob ()
end;
- let _ = Coqloop.loop ~time:opts.time ~state in
+ let _ = Coqloop.loop ~state in
(* Initialise and launch the Ocaml toplevel *)
Coqinit.init_ocaml_path();
Mltop.ocaml_toploop();
@@ -95,7 +95,7 @@ let load_vernacular opts ~state =
(fun state (f_in, echo) ->
let s = Loadpath.locate_file f_in in
(* Should make the beautify logic clearer *)
- let load_vernac f = Vernac.load_vernac ~time:opts.time ~echo ~interactive:false ~check:true ~state f in
+ let load_vernac f = Vernac.load_vernac ~echo ~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
@@ -103,7 +103,7 @@ let load_vernacular opts ~state =
let load_init_vernaculars opts ~state =
let state = if opts.load_rcfile then
- Coqinit.load_rcfile ~rcfile:opts.rcfile ~time:opts.time ~state
+ Coqinit.load_rcfile ~rcfile:opts.rcfile ~state
else begin
Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading.");
state
@@ -223,7 +223,7 @@ let compile opts ~echo ~f_in ~f_out =
iload_path; require_libs; stm_options;
}) in
- let state = { doc; sid; proof = None } in
+ let state = { doc; sid; proof = None; time = opts.time } in
let state = load_init_vernaculars opts ~state in
let ldir = Stm.get_ldir ~doc:state.doc in
Aux_file.(start_aux_file
@@ -232,7 +232,7 @@ let compile opts ~echo ~f_in ~f_out =
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 state = Vernac.load_vernac ~time:opts.time ~echo ~check:true ~interactive:false ~state long_f_dot_v in
+ let state = Vernac.load_vernac ~echo ~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 ();
@@ -270,10 +270,10 @@ let compile opts ~echo ~f_in ~f_out =
iload_path; require_libs; stm_options;
}) in
- let state = { doc; sid; proof = None } in
+ let state = { doc; sid; proof = None; time = opts.time } 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 ~echo ~check:false ~interactive:false ~state long_f_dot_v in
+ let state = Vernac.load_vernac ~echo ~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
@@ -476,7 +476,7 @@ let init_toplevel arglist =
{ doc_type = Interactive opts.toplevel_name;
iload_path; require_libs; stm_options;
}) in
- let state = { doc; sid; proof = None } in
+ let state = { doc; sid; proof = None; time = opts.time } 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 *)
diff --git a/toplevel/g_toplevel.ml4 b/toplevel/g_toplevel.ml4
new file mode 100644
index 000000000..7526f3071
--- /dev/null
+++ b/toplevel/g_toplevel.ml4
@@ -0,0 +1,43 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Pcoq
+open Vernacexpr
+
+(* Vernaculars specific to the toplevel *)
+type vernac_toplevel =
+ | VernacDrop
+ | VernacQuit
+ | VernacControl of vernac_control
+
+module Toplevel_ : sig
+ val vernac_toplevel : vernac_toplevel CAst.t Gram.entry
+end = struct
+ let gec_vernac s = Gram.entry_create ("toplevel:" ^ s)
+ let vernac_toplevel = gec_vernac "vernac_toplevel"
+end
+
+open Toplevel_
+
+GEXTEND Gram
+ GLOBAL: vernac_toplevel;
+ vernac_toplevel: FIRST
+ [ [ IDENT "Drop"; "." -> CAst.make VernacDrop
+ | IDENT "Quit"; "." -> CAst.make VernacQuit
+ | cmd = main_entry ->
+ match cmd with
+ | None -> raise Stm.End_of_input
+ | Some (loc,c) -> CAst.make ~loc (VernacControl c)
+ ]
+ ]
+ ;
+END
+
+let parse_toplevel pa = Pcoq.Gram.entry_parse vernac_toplevel pa
diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib
index 9fb2e33d7..78b96e5e2 100644
--- a/toplevel/toplevel.mllib
+++ b/toplevel/toplevel.mllib
@@ -1,5 +1,6 @@
Vernac
Usage
+G_toplevel
Coqloop
Coqinit
Coqargs
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index fdd0d4ed3..c1bbb20d5 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -28,10 +28,6 @@ let checknav_deep {CAst.loc;v=ast} =
if is_deep_navigation_vernac ast then
CErrors.user_err ?loc (str "Navigation commands forbidden in nested commands.")
-let disable_drop = function
- | Drop -> CErrors.user_err Pp.(str "Drop is forbidden.")
- | e -> e
-
(* Echo from a buffer based on position.
XXX: Should move to utility file. *)
let vernac_echo ?loc in_chan = let open Loc in
@@ -80,17 +76,21 @@ module State = struct
doc : Stm.doc;
sid : Stateid.t;
proof : Proof.t option;
+ time : bool;
}
end
-let interp_vernac ~time ~check ~interactive ~state ({CAst.loc;_} as com) =
+let interp_vernac ~check ~interactive ~state ({CAst.loc;_} as com) =
let open State in
try
(* The -time option is only supported from console-based clients
due to the way it prints. *)
- if time then print_cmd_header com;
- let com = if time then CAst.make ?loc @@ VernacTime(time,com) else com in
+ let com = if state.time
+ then begin
+ print_cmd_header com;
+ CAst.make ?loc @@ VernacTime(state.time,com)
+ end else com in
let doc, nsid, ntip = Stm.add ~doc:state.doc ~ontop:state.sid (not !Flags.quiet) com in
(* Main STM interaction *)
@@ -102,7 +102,7 @@ let interp_vernac ~time ~check ~interactive ~state ({CAst.loc;_} as com) =
(* Stm.observe nsid; *)
let ndoc = if check then Stm.finish ~doc else doc in
let new_proof = Proof_global.give_me_the_proof_opt () in
- { doc = ndoc; sid = nsid; proof = new_proof }
+ { state with doc = ndoc; sid = nsid; proof = new_proof; }
with reraise ->
(* XXX: In non-interactive mode edit_at seems to do very weird
things, so we better avoid it while we investigate *)
@@ -115,7 +115,7 @@ let interp_vernac ~time ~check ~interactive ~state ({CAst.loc;_} as com) =
end in iraise (reraise, info)
(* Load a vernac file. CErrors are annotated with file and location *)
-let load_vernac_core ~time ~echo ~check ~interactive ~state file =
+let load_vernac_core ~echo ~check ~interactive ~state file =
(* Keep in sync *)
let in_chan = open_utf8_file_in file in
let in_echo = if echo then Some (open_utf8_file_in file) else None in
@@ -154,7 +154,7 @@ let load_vernac_core ~time ~echo ~check ~interactive ~state file =
Option.iter (vernac_echo ?loc) in_echo;
checknav_simple ast;
- let state = Flags.silently (interp_vernac ~time ~check ~interactive ~state:!rstate) ast in
+ let state = Flags.silently (interp_vernac ~check ~interactive ~state:!rstate) ast in
rids := state.sid :: !rids;
rstate := state;
done;
@@ -165,11 +165,11 @@ let load_vernac_core ~time ~echo ~check ~interactive ~state file =
input_cleanup ();
match e with
| Stm.End_of_input -> !rstate, !rids, Pcoq.Gram.comment_state in_pa
- | reraise -> iraise (disable_drop e, info)
+ | reraise -> iraise (e, info)
-let process_expr ~time ~state loc_ast =
+let process_expr ~state loc_ast =
checknav_deep loc_ast;
- interp_vernac ~time ~interactive:true ~check:true ~state loc_ast
+ interp_vernac ~interactive:true ~check:true ~state loc_ast
(******************************************************************************)
(* Beautify-specific code *)
@@ -220,8 +220,8 @@ let beautify_pass ~doc ~comments ~ids ~filename =
(* Main driver for file loading. For now, we only do one beautify
pass. *)
-let load_vernac ~time ~echo ~check ~interactive ~state filename =
- let ostate, ids, comments = load_vernac_core ~time ~echo ~check ~interactive ~state filename in
+let load_vernac ~echo ~check ~interactive ~state filename =
+ let ostate, ids, comments = load_vernac_core ~echo ~check ~interactive ~state filename in
(* Pass for beautify *)
if !Flags.beautify then beautify_pass ~doc:ostate.State.doc ~comments ~ids:List.(rev ids) ~filename;
(* End pass *)
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index 51758642e..126954023 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -15,6 +15,7 @@ module State : sig
doc : Stm.doc;
sid : Stateid.t;
proof : Proof.t option;
+ time : bool;
}
end
@@ -23,10 +24,10 @@ end
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 -> state:State.t -> Vernacexpr.vernac_control CAst.t -> State.t
+val process_expr : state:State.t -> Vernacexpr.vernac_control CAst.t -> 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 -> echo:bool -> check:bool -> interactive:bool ->
+val load_vernac : echo:bool -> check:bool -> interactive:bool ->
state:State.t -> string -> State.t
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 3dbe8b0c0..9ff4e3302 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2010,9 +2010,6 @@ let interp ?proof ~atts ~st c =
| VernacUndoTo _ -> CErrors.user_err (str "UndoTo cannot be used through the Load command")
| VernacBacktrack _ -> CErrors.user_err (str "Backtrack cannot be used through the Load command")
- (* Toplevel control *)
- | VernacToplevelControl e -> raise e
-
(* Resetting *)
| VernacResetName _ -> anomaly (str "VernacResetName not handled by Stm.")
| VernacResetInitial -> anomaly (str "VernacResetInitial not handled by Stm.")
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index 1f2d2e4b4..d4f2a753f 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -79,7 +79,6 @@ let call opn converted_args ~atts ~st =
phase := "Executing command";
hunk ~atts ~st
with
- | Drop -> raise Drop
| reraise ->
let reraise = CErrors.push reraise in
if !Flags.debug then
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 01:04:51 +0000