aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/coqtop.ml40
-rw-r--r--toplevel/vernac.ml78
2 files changed, 60 insertions, 58 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 712efbbd5..db7bcb76b 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -8,7 +8,6 @@
open Pp
open CErrors
-open Flags
open Libnames
open Coqinit
@@ -31,7 +30,7 @@ let print_header () =
Feedback.msg_notice (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")");
flush_all ()
-let warning s = with_option Flags.warn Feedback.msg_warning (strbrk s)
+let warning s = Flags.(with_option warn Feedback.msg_warning (strbrk s))
let toploop = ref None
@@ -87,7 +86,7 @@ let console_toploop_run () =
(* 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
- if_verbose warning "Dumpglob cannot be used in interactive mode.";
+ Flags.if_verbose warning "Dumpglob cannot be used in interactive mode.";
Dumpglob.noglob ()
end;
Coqloop.loop();
@@ -130,7 +129,7 @@ let set_type_in_type () =
let engage () =
Global.set_engagement !impredicative_set
-let set_batch_mode () = batch_mode := true
+let set_batch_mode () = Flags.batch_mode := true
let toplevel_default_name = Names.(DirPath.make [Id.of_string "Top"])
let toplevel_name = ref toplevel_default_name
@@ -177,7 +176,7 @@ let load_vernacular sid =
(fun sid (s,v) ->
let s = Loadpath.locate_file s in
if !Flags.beautify then
- with_option beautify_file (Vernac.load_vernac v sid) s
+ Flags.(with_option beautify_file (Vernac.load_vernac v sid) s)
else
Vernac.load_vernac v sid s)
sid (List.rev !load_vernacular_list)
@@ -199,7 +198,7 @@ let require_prelude () =
let require_list = ref ([] : string list)
let add_require s = require_list := s :: !require_list
let require () =
- let () = if !load_init then silently require_prelude () in
+ let () = if !Flags.load_init then Flags.silently require_prelude () in
let map dir = Qualid (Loc.tag @@ qualid_of_string dir) in
Vernacentries.vernac_require None (Some false) (List.rev_map map !require_list)
@@ -229,7 +228,7 @@ let add_compile verbose s =
let compile_file (v,f) =
if !Flags.beautify then
- with_option beautify_file (Vernac.compile v) f
+ Flags.(with_option beautify_file (Vernac.compile v) f)
else
Vernac.compile v f
@@ -304,7 +303,7 @@ let usage () =
init_load_path ();
with NoCoqLib -> usage_no_coqlib ()
end;
- if !batch_mode then Usage.print_usage_coqc ()
+ if !Flags.batch_mode then Usage.print_usage_coqc ()
else begin
Mltop.load_ml_objects_raw_rex
(Str.regexp (if Mltop.is_native then "^.*top.cmxs$" else "^.*top.cma$"));
@@ -538,7 +537,7 @@ let parse_args arglist =
|"-with-geoproof" -> Coq_config.with_geoproof := get_bool opt (next ())
|"-main-channel" -> Spawned.main_channel := get_host_port opt (next())
|"-control-channel" -> Spawned.control_channel := get_host_port opt (next())
- |"-vio2vo" -> add_compile false (next ()); Flags.compilation_mode := Vio2Vo
+ |"-vio2vo" -> add_compile false (next ()); Flags.compilation_mode := Flags.Vio2Vo
|"-toploop" -> set_toploop (next ())
|"-w" | "-W" ->
let w = next () in
@@ -556,9 +555,9 @@ let parse_args arglist =
|"-async-proofs-never-reopen-branch" ->
Flags.async_proofs_never_reopen_branch := true;
|"-batch" -> set_batch_mode ()
- |"-test-mode" -> test_mode := true
- |"-beautify" -> beautify := true
- |"-boot" -> boot := true; no_load_rc ()
+ |"-test-mode" -> Flags.test_mode := true
+ |"-beautify" -> Flags.beautify := true
+ |"-boot" -> Flags.boot := true; no_load_rc ()
|"-bt" -> Backtrace.record_backtrace true
|"-color" -> set_color (next ())
|"-config"|"--config" -> print_config := true
@@ -570,19 +569,18 @@ let parse_args arglist =
|"-ideslave" -> set_ideslave ()
|"-impredicative-set" -> set_impredicative_set ()
|"-indices-matter" -> Indtypes.enforce_indices_matter ()
- |"-just-parsing" -> warning "-just-parsing option has been removed in 8.6"
|"-m"|"--memory" -> memory_stat := true
- |"-noinit"|"-nois" -> load_init := false
+ |"-noinit"|"-nois" -> Flags.load_init := false
|"-no-glob"|"-noglob" -> Dumpglob.noglob (); glob_opt := true
|"-native-compiler" ->
if Coq_config.no_native_compiler then
warning "Native compilation was disabled at configure time."
- else native_compiler := true
+ else Flags.native_compiler := true
|"-output-context" -> output_context := true
|"-profile-ltac" -> Flags.profile_ltac := true
|"-q" -> no_load_rc ()
|"-quiet"|"-silent" -> Flags.quiet := true; Flags.make_warn false
- |"-quick" -> Flags.compilation_mode := BuildVio
+ |"-quick" -> Flags.compilation_mode := Flags.BuildVio
|"-list-tags" -> print_tags := true
|"-time" -> Flags.time := true
|"-type-in-type" -> set_type_in_type ()
@@ -625,11 +623,11 @@ let init_toplevel arglist =
prerr_endline "See -help for the list of supported options";
exit 1
end;
- if_verbose print_header ();
+ Flags.if_verbose print_header ();
inputstate ();
Mltop.init_known_plugins ();
engage ();
- if (not !batch_mode || CList.is_empty !compile_list)
+ if (not !Flags.batch_mode || CList.is_empty !compile_list)
&& Global.env_is_initial ()
then Declaremods.start_library !toplevel_name;
init_library_roots ();
@@ -650,16 +648,16 @@ let init_toplevel arglist =
with any ->
flush_all();
let extra =
- if !batch_mode && not Stateid.(equal (Stm.get_current_state ()) dummy)
+ if !Flags.batch_mode && not Stateid.(equal (Stm.get_current_state ()) dummy)
then None
else Some (str "Error during initialization: ")
in
fatal_error ?extra any
end;
- if !batch_mode then begin
+ if !Flags.batch_mode then begin
flush_all();
if !output_context then
- Feedback.msg_notice (with_option raw_print Prettyp.print_full_pure_context () ++ fnl ());
+ Feedback.msg_notice Flags.(with_option raw_print Prettyp.print_full_pure_context () ++ fnl ());
Profile.print_profile ();
exit 0
end;
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 1602f9c68..1b020bc87 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -11,7 +11,6 @@
open Pp
open CErrors
open Util
-open Flags
open Vernacexpr
open Vernacprop
@@ -48,35 +47,29 @@ let beautify_suffix = ".beautified"
let set_formatter_translator ch =
let out s b e = output_substring ch s b e in
- Format.set_formatter_output_functions out (fun () -> flush ch);
- Format.set_max_boxes max_int
+ let ft = Format.make_formatter out (fun () -> flush ch) in
+ Format.pp_set_max_boxes ft max_int;
+ ft
-let pr_new_syntax_in_context ?loc chan_beautify ocom =
+let pr_new_syntax_in_context ?loc ft_beautify ocom =
let loc = Option.cata Loc.unloc (0,0) loc in
- if !beautify_file then set_formatter_translator chan_beautify;
let fs = States.freeze ~marshallable:`No in
- (* The content of this is not supposed to fail, but if ever *)
- try
- (* Side-effect: order matters *)
- let before = comment (CLexer.extract_comments (fst loc)) in
- let com = match ocom with
- | Some com -> Ppvernac.pr_vernac com
- | None -> mt() in
- let after = comment (CLexer.extract_comments (snd loc)) in
- if !beautify_file then
- (Pp.pp_with !Topfmt.std_ft (hov 0 (before ++ com ++ after));
- Format.pp_print_flush !Topfmt.std_ft ())
- else
- Feedback.msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com)));
- States.unfreeze fs;
- Format.set_formatter_out_channel stdout
- with any ->
- States.unfreeze fs;
- Format.set_formatter_out_channel stdout
-
-let pr_new_syntax ?loc po chan_beautify ocom =
+ (* Side-effect: order matters *)
+ let before = comment (CLexer.extract_comments (fst loc)) in
+ let com = match ocom with
+ | Some com -> Ppvernac.pr_vernac com
+ | None -> mt() in
+ let after = comment (CLexer.extract_comments (snd loc)) in
+ if !Flags.beautify_file then
+ (Pp.pp_with ft_beautify (hov 0 (before ++ com ++ after));
+ Format.pp_print_flush ft_beautify ())
+ else
+ Feedback.msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com)));
+ States.unfreeze fs
+
+let pr_new_syntax ?loc po ft_beautify ocom =
(* Reinstall the context of parsing which includes the bindings of comments to locations *)
- Pcoq.Gram.with_parsable po (pr_new_syntax_in_context ?loc chan_beautify) ocom
+ Pcoq.Gram.with_parsable po (pr_new_syntax_in_context ?loc ft_beautify) ocom
(* For coqtop -time, we display the position in the file,
and a glimpse of the executed command *)
@@ -133,10 +126,16 @@ let rec interp_vernac sid (loc,com) =
highly dynamic and depends on the structure of the
document. Hopefully this is fixed when VtBack can be removed
and Undo etc... are just interpreted regularly. *)
+
+ (* XXX: The classifier can emit warnings so we need to guard
+ against that... *)
+ let wflags = CWarnings.get_flags () in
+ CWarnings.set_flags "none";
let is_proof_step = match fst (Vernac_classifier.classify_vernac v) with
- | VtProofStep _ | VtStm (VtBack _, _) | VtStartProof _ -> true
+ | VtProofStep _ | VtBack (_, _) | VtStartProof _ -> true
| _ -> false
in
+ CWarnings.set_flags wflags;
let nsid, ntip = Stm.add ~ontop:sid (not !Flags.quiet) (loc,v) in
@@ -178,8 +177,13 @@ let rec interp_vernac sid (loc,com) =
(* Load a vernac file. CErrors are annotated with file and location *)
and load_vernac verbosely sid file =
- let chan_beautify =
- if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout in
+ let ft_beautify, close_beautify =
+ if !Flags.beautify_file then
+ let chan_beautify = open_out (file^beautify_suffix) in
+ set_formatter_translator chan_beautify, fun () -> close_out chan_beautify;
+ else
+ !Topfmt.std_ft, fun () -> ()
+ 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:(Loc.InFile file) (Stream.of_channel in_chan) in
@@ -209,7 +213,7 @@ and load_vernac verbosely sid file =
*)
in
(* Printing of vernacs *)
- if !beautify then pr_new_syntax ?loc in_pa chan_beautify (Some ast);
+ if !Flags.beautify then pr_new_syntax ?loc in_pa ft_beautify (Some ast);
Option.iter (vernac_echo ?loc) in_echo;
checknav_simple (loc, ast);
@@ -224,12 +228,12 @@ and load_vernac verbosely sid file =
match e with
| Stm.End_of_input ->
(* Is this called so comments at EOF are printed? *)
- if !beautify then
- pr_new_syntax ~loc:(Loc.make_loc (max_int,max_int)) in_pa chan_beautify None;
- if !Flags.beautify_file then close_out chan_beautify;
+ 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 ();
!rsid
| reraise ->
- if !Flags.beautify_file then close_out chan_beautify;
+ if !Flags.beautify_file then close_beautify ();
iraise (disable_drop e, info)
(** [eval_expr : ?preserving:bool -> Loc.t * Vernacexpr.vernac_expr -> unit]
@@ -290,7 +294,7 @@ let compile verbosely f =
++ str ".")
in
match !Flags.compilation_mode with
- | BuildVo ->
+ | Flags.BuildVo ->
let long_f_dot_v = ensure_v f in
ensure_exists long_f_dot_v;
let long_f_dot_vo =
@@ -314,7 +318,7 @@ let compile verbosely f =
(Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
Aux_file.stop_aux_file ();
Dumpglob.end_dump_glob ()
- | BuildVio ->
+ | Flags.BuildVio ->
let long_f_dot_v = ensure_v f in
ensure_exists long_f_dot_v;
let long_f_dot_vio =
@@ -329,7 +333,7 @@ let compile verbosely f =
check_pending_proofs ();
Stm.snapshot_vio ldir long_f_dot_vio;
Stm.reset_task_queue ()
- | Vio2Vo ->
+ | Flags.Vio2Vo ->
let open Filename in
let open Library in
Dumpglob.noglob ();
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 06:39:40 +0000