diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqargs.ml | 2 | ||||
| -rw-r--r-- | toplevel/coqloop.ml | 11 | ||||
| -rw-r--r-- | toplevel/coqloop.mli | 3 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 4 | ||||
| -rw-r--r-- | toplevel/coqtop.mli | 3 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 28 |
6 files changed, 24 insertions, 27 deletions
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 5b73471c5..a7065c031 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -153,7 +153,7 @@ let add_compat_require opts v = let set_batch_mode opts = Flags.quiet := true; - System.trust_file_cache := false; + System.trust_file_cache := true; { opts with batch_mode = true } let add_compile opts verbose s = diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index ae0b94476..7ad8e2c05 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -339,6 +339,8 @@ let loop_flush_all () = Format.pp_print_flush !Topfmt.std_ft (); Format.pp_print_flush !Topfmt.err_ft () +let drop_last_doc = ref None + let rec loop ~time ~state = let open Vernac.State in Sys.catch_break true; @@ -353,7 +355,14 @@ let rec loop ~time ~state = not possible due exceptions. *) in vernac_loop ~state with - | CErrors.Drop -> state + | 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 | any -> top_stderr (str "Anomaly: main loop exited with exception: " ++ diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli index 1c1309051..928f3609a 100644 --- a/toplevel/coqloop.mli +++ b/toplevel/coqloop.mli @@ -35,3 +35,6 @@ 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 + +(** 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 26ede1834..deb2c2038 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -34,7 +34,6 @@ let warning s = Flags.(with_option warn Feedback.msg_warning (strbrk s)) will not be generally be initialized, thus stateid, etc... may be bogus. For now we just print to the console too *) let coqtop_init_feed = Coqloop.coqloop_feed -let drop_last_doc = ref None (* Default toplevel loop *) let console_toploop_run opts ~state = @@ -44,9 +43,8 @@ let console_toploop_run opts ~state = Flags.if_verbose warning "Dumpglob cannot be used in interactive mode."; Dumpglob.noglob () end; - let state = Coqloop.loop ~time:opts.time ~state in + let _ = Coqloop.loop ~time:opts.time ~state in (* Initialise and launch the Ocaml toplevel *) - drop_last_doc := Some state; Coqinit.init_ocaml_path(); Mltop.ocaml_toploop(); (* We let the feeder in place for users of Drop *) diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index dedb298e2..510e10dd1 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -15,9 +15,6 @@ 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 : 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 -> state:Vernac.State.t -> unit) ref diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 92dee84f3..a84990f91 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -120,16 +120,9 @@ module State = struct end -let rec interp_vernac ~time ~check ~interactive ~state (loc,com) = +let 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 ~state f - | _ -> + try (* XXX: We need to run this before add as the classification is highly dynamic and depends on the structure of the document. Hopefully this is fixed when VtMeta can be removed @@ -139,13 +132,17 @@ let rec interp_vernac ~time ~check ~interactive ~state (loc,com) = against that... *) let wflags = CWarnings.get_flags () in CWarnings.set_flags "none"; - let is_proof_step = match fst (Vernac_classifier.classify_vernac v) with + let is_proof_step = match fst (Vernac_classifier.classify_vernac com) with | VtProofStep _ | VtMeta | VtStartProof _ -> true | _ -> false in CWarnings.set_flags wflags; - let doc, nsid, ntip = Stm.add ~doc:state.doc ~ontop:state.sid (not !Flags.quiet) (loc,v) in + (* The -time option is only supported from console-based + clients due to the way it prints. *) + if time then print_cmd_header ?loc com; + let com = if time then VernacTime(time,(CAst.make ?loc com)) else com in + let doc, nsid, ntip = Stm.add ~doc:state.doc ~ontop:state.sid (not !Flags.quiet) (loc,com) in (* Main STM interaction *) if ntip <> `NewTip then @@ -165,13 +162,6 @@ let rec interp_vernac ~time ~check ~interactive ~state (loc,com) = if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ()); 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 - clients due to the way it prints. *) - if time then print_cmd_header ?loc com; - let com = if time then VernacTime(time, CAst.make ?loc com) else com in - interp com with reraise -> (* XXX: In non-interactive mode edit_at seems to do very weird things, so we better avoid it while we investigate *) @@ -184,7 +174,7 @@ let rec interp_vernac ~time ~check ~interactive ~state (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 ~state file = +let 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 |