From fb482f6b02156c1fcf029263083b0371e030a2cd Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 20 Sep 2017 08:30:24 +0200 Subject: [flags] Flag `open Flags` An incoming commit is removing some toplevel-specific global flags in favor of local toplevel state; this commit flags `Flags` use so it becomes clearer in the code whether we are relying on some "global" settable status in code. A good candidate for further cleanup is the pattern: `Flags.if_verbose Feedback.msg_info` --- toplevel/coqtop.ml | 39 +++++++++++++++++++-------------------- toplevel/vernac.ml | 15 +++++++-------- 2 files changed, 26 insertions(+), 28 deletions(-) (limited to 'toplevel') diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 0f8524e92..57902cb27 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" -> CWarnings.set_flags (CWarnings.normalize_flags_string (next ())) |"-o" -> Flags.compilation_output_name := Some (next()) @@ -551,9 +550,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 @@ -567,17 +566,17 @@ let parse_args arglist = |"-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 () @@ -620,11 +619,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 (); @@ -645,16 +644,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..c33f6b9b8 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 @@ -53,7 +52,7 @@ let set_formatter_translator ch = let pr_new_syntax_in_context ?loc chan_beautify ocom = let loc = Option.cata Loc.unloc (0,0) loc in - if !beautify_file then set_formatter_translator chan_beautify; + if !Flags.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 @@ -63,7 +62,7 @@ let pr_new_syntax_in_context ?loc chan_beautify ocom = | Some com -> Ppvernac.pr_vernac com | None -> mt() in let after = comment (CLexer.extract_comments (snd loc)) in - if !beautify_file then + if !Flags.beautify_file then (Pp.pp_with !Topfmt.std_ft (hov 0 (before ++ com ++ after)); Format.pp_print_flush !Topfmt.std_ft ()) else @@ -209,7 +208,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 chan_beautify (Some ast); Option.iter (vernac_echo ?loc) in_echo; checknav_simple (loc, ast); @@ -224,7 +223,7 @@ 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 + if !Flags.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; !rsid @@ -290,7 +289,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 +313,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 +328,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 (); -- cgit v1.2.3