diff options
author | 2001-04-03 08:04:19 +0000 | |
---|---|---|
committer | 2001-04-03 08:04:19 +0000 | |
commit | bb76b246d1396f788d18888abe8284befb7f44b9 (patch) | |
tree | b7dd5667977ceae4f3944945a55cac6412681abb /toplevel | |
parent | 78811c7ecba58fc35a3441ac1d510c67e28b159e (diff) |
utilisation de Options.if_verbose
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1519 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
-rw-r--r-- | toplevel/command.ml | 23 | ||||
-rw-r--r-- | toplevel/coqinit.ml | 4 | ||||
-rw-r--r-- | toplevel/coqtop.ml | 2 | ||||
-rw-r--r-- | toplevel/discharge.ml | 4 | ||||
-rw-r--r-- | toplevel/mltop.ml4 | 8 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 40 |
6 files changed, 38 insertions, 43 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index a5b1b3b1d..c7fcc0f3b 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -67,8 +67,7 @@ let declare_global_definition ident ce n local = let sp = declare_constant ident (ConstantEntry ce,n,false) in if local then wARNING [< pr_id ident; 'sTR" is declared as a global definition" >]; - if is_verbose() then - message ((string_of_id ident) ^ " is defined"); + if_verbose message ((string_of_id ident) ^ " is defined"); ConstRef sp let definition_body_red red_option ident (local,n) com comtypeopt = @@ -80,7 +79,7 @@ let definition_body_red red_option ident (local,n) com comtypeopt = if Lib.is_section_p disch_sp then begin let c = constr_of_constr_entry ce' in let sp = declare_variable ident (SectionLocalDef c,n,false) in - if is_verbose() then message ((string_of_id ident) ^ " is defined"); + if_verbose message ((string_of_id ident) ^ " is defined"); if Pfedit.refining () then mSGERRNL [< 'sTR"Warning: Local definition "; pr_id ident; 'sTR" is not visible from current goals" >]; @@ -97,15 +96,14 @@ let definition_body = definition_body_red None let syntax_definition ident com = let c = interp_rawconstr Evd.empty (Global.env()) com in Syntax_def.declare_syntactic_definition ident c; - if is_verbose() then - message ((string_of_id ident) ^ " is now a syntax macro") + if_verbose message ((string_of_id ident) ^ " is now a syntax macro") (* 2| Variable definitions *) let parameter_def_var ident c = let c = interp_type Evd.empty (Global.env()) c in let sp = declare_parameter (id_of_string ident) c in - if is_verbose() then message (ident ^ " is assumed"); + if_verbose message (ident ^ " is assumed"); sp let declare_global_assumption ident c = @@ -122,7 +120,7 @@ let hypothesis_def_var is_refining ident n c = let t = interp_type Evd.empty (Global.env()) c in let sp = declare_variable (id_of_string ident) (SectionLocalAssum t,n,false) in - if is_verbose() then message (ident ^ " is assumed"); + if_verbose message (ident ^ " is assumed"); if is_refining then mSGERRNL [< 'sTR"Warning: Variable "; 'sTR ident; 'sTR" is not visible from current goals" >]; @@ -214,7 +212,7 @@ let declare_mutual_with_eliminations mie = let lrecnames = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in let sp = declare_mind mie in - if is_verbose() then pPNL(minductive_message lrecnames); + if_verbose pPNL (minductive_message lrecnames); declare_eliminations sp; sp @@ -309,7 +307,7 @@ let build_recursive lnameargsardef = in (* declare the recursive definitions *) let lrefrec = declare 0 lnamerec in - if is_verbose() then pPNL(recursive_message lrefrec) + if_verbose pPNL (recursive_message lrefrec) end; (* The others are declared as normal definitions *) let var_subst id = (id, global_reference CCI id) in @@ -377,7 +375,7 @@ let build_corecursive lnameardef = | _ -> [] in let lrefrec = declare 0 lnamerec in - if is_verbose() then pPNL(corecursive_message lrefrec) + if_verbose pPNL (corecursive_message lrefrec) end; let var_subst id = (id, global_reference CCI id) in let _ = @@ -422,7 +420,7 @@ let build_scheme lnamedepindsort = ConstRef sp :: lrecref in let lrecref = List.fold_right2 declare listdecl lrecnames [] in - if is_verbose() then pPNL(recursive_message lrecref) + if_verbose pPNL (recursive_message lrecref) let start_proof_com sopt stre com = let env = Global.env () in @@ -456,8 +454,7 @@ let save opacity id ({const_entry_body = pft; const_entry_type = tpo} as const) if not (strength = NotDeclare) then begin Pfedit.delete_current_proof (); - if Options.is_verbose() then - message ((string_of_id id) ^ " is defined") + if_verbose message ((string_of_id id) ^ " is defined") end let save_named opacity = diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 133029253..7b3fa1628 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -39,7 +39,7 @@ let load_rcfile() = Vernac.load_vernac false !rcfile else () (* - if Options.is_verbose() then + Options.if_verbose mSGNL [< 'sTR ("No .coqrc or .coqrc."^Coq_config.version^ " found. Skipping rcfile loading.") >] *) @@ -47,7 +47,7 @@ let load_rcfile() = (mSGNL [< 'sTR"Load of rcfile failed." >]; raise e) else - if Options.is_verbose() then mSGNL [< 'sTR"Skipping rcfile loading." >] + Options.if_verbose mSGNL [< 'sTR"Skipping rcfile loading." >] let add_ml_include s = Mltop.add_ml_dir s diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index f1cc40461..0778b7735 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -197,7 +197,7 @@ let start () = Lib.init(); try parse_args (); - if is_verbose() then print_header (); + if_verbose print_header (); init_load_path (); inputstate (); init_library_roots (); diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index fdaf56706..a4ab22eed 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -141,10 +141,10 @@ let process_inductive osecsp nsecsp oldenv (ids_to_discard,modlist) mib = (* Discharge messages. *) let constant_message id = - if Options.is_verbose() then pPNL [< pr_id id; 'sTR " is discharged." >] + Options.if_verbose pPNL [< pr_id id; 'sTR " is discharged." >] let inductive_message inds = - if Options.is_verbose() then + Options.if_verbose pPNL (hOV 0 (match inds with diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index b3508f85f..531e52752 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -10,6 +10,7 @@ open Util open Pp +open Options open System open Libobject open Library @@ -246,11 +247,12 @@ let cache_ml_module_object (_,{mnames=mnames}) = let fname = file_of_name mname in begin try - mSG [< 'sTR"[Loading ML file " ; 'sTR fname ; 'sTR" ..." >]; + if_verbose + mSG [< 'sTR"[Loading ML file "; 'sTR fname; 'sTR" ..." >]; load_object mname fname; - mSGNL [< 'sTR"done]" >] + if_verbose mSGNL [< 'sTR"done]" >] with e -> - pPNL [< 'sTR"failed]" >]; + if_verbose mSGNL [< 'sTR"failed]" >]; raise e end; add_loaded_module mname) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 2b69fca48..c7b68ecea 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -384,7 +384,7 @@ let _ = | [VARG_IDENTIFIER id] -> (fun () -> check_no_pending_proofs (); - Discharge.close_section (not (is_silent())) (string_of_id id)) + Discharge.close_section (is_verbose ()) (string_of_id id)) | _ -> bad_vernac_args "EndSection") (* Proof switching *) @@ -396,7 +396,7 @@ let _ = (fun () -> if not (refining()) then begin start_proof_com None NeverDischarge com; - if not (is_silent()) then show_open_subgoals () + if_verbose show_open_subgoals () end else error "repeated Goal not permitted in refining mode") | [] -> (fun () -> ()) @@ -579,14 +579,14 @@ let _ = add "SaveNamed" (function | [] -> - (fun () -> if not(is_silent()) then show_script(); save_named true) + (fun () -> if_verbose show_script (); save_named true) | _ -> bad_vernac_args "SaveNamed") let _ = add "DefinedNamed" (function | [] -> - (fun () -> if not(is_silent()) then show_script(); save_named false) + (fun () -> if_verbose show_script (); save_named false) | _ -> bad_vernac_args "DefinedNamed") let _ = @@ -594,7 +594,7 @@ let _ = (function | [VARG_IDENTIFIER id] -> (fun () -> - if not(is_silent()) then show_script(); + if_verbose show_script (); save_anonymous false (string_of_id id)) | _ -> bad_vernac_args "DefinedAnonymous") @@ -603,7 +603,7 @@ let _ = (function | [VARG_IDENTIFIER id] -> (fun () -> - if not(is_silent()) then show_script(); + if_verbose show_script (); save_anonymous true (string_of_id id)) | _ -> bad_vernac_args "SaveAnonymous") @@ -612,7 +612,7 @@ let _ = (function | [VARG_IDENTIFIER id] -> (fun () -> - if not(is_silent()) then show_script(); + if_verbose show_script (); save_anonymous_thm true (string_of_id id)) | _ -> bad_vernac_args "SaveAnonymousThm") @@ -621,7 +621,7 @@ let _ = (function | [VARG_IDENTIFIER id] -> (fun () -> - if not(is_silent()) then show_script(); + if_verbose show_script (); save_anonymous_remark true (string_of_id id)) | _ -> bad_vernac_args "SaveAnonymousRmk") @@ -635,8 +635,7 @@ let _ = id_list) let warning_opaque s = - if not(is_silent()) then - warning + if_verbose warning ("This command turns the constants which depend on the definition/proof of "^s^" un-re-checkable until the next \"Transparent "^s^"\" command.") @@ -869,7 +868,7 @@ let _ = errorlabstrm "Vernacentries.StartProof" [< 'sTR "Let declarations can only be used in proof editing mode" >]; start_proof_com (Some s) stre com; - if not (is_silent()) then show_open_subgoals() + if_verbose show_open_subgoals () end | _ -> bad_vernac_args "StartProof") @@ -900,9 +899,9 @@ let _ = States.with_heavy_rollback (fun () -> start_proof_com (Some s) stre com; - if not (is_silent()) then show_open_subgoals(); + if_verbose show_open_subgoals (); List.iter Vernacinterp.call calls; - if not (is_silent()) then show_script(); + if_verbose show_script (); if not (kind = "LETTOP") then save_named opacity else @@ -959,8 +958,7 @@ let _ = definition_body_red red_option id (local,stre) c typ_opt in if coe then begin Class.try_add_new_coercion ref stre; - if not (is_silent()) then - message ((string_of_id id) ^ " is now a coercion") + if_verbose message ((string_of_id id) ^ " is now a coercion") end; if idcoe then begin let cl = Class.class_of_ref ref in @@ -1332,7 +1330,7 @@ let _ = | _ -> bad_vernac_args "") l) in abstraction_definition id arity com; - if (not(is_silent())) then + if_verbose message ((string_of_id id)^" is now an abstraction")) | _ -> bad_vernac_args "ABSTRACTION") ***) @@ -1387,8 +1385,7 @@ let _ = fun () -> let ref = locate_qualid dummy_loc qid in Class.try_add_new_class ref stre; - if not (is_silent()) then - message ((string_of_qualid qid) ^ " is now a class") + if_verbose message ((string_of_qualid qid) ^ " is now a class") | _ -> bad_vernac_args "CLASS") let cl_of_qualid qid = @@ -1419,8 +1416,8 @@ let _ = else let ref = locate_qualid dummy_loc qid in Class.try_add_new_coercion_with_target ref stre source target; - if not (is_silent()) then - message ((string_of_qualid qid) ^ " is now a coercion") + if_verbose + message ((string_of_qualid qid) ^ " is now a coercion") | _ -> bad_vernac_args "COERCION") let _ = @@ -1745,8 +1742,7 @@ let _ = save_named true) | _ -> assert false) -let print_subgoals () = - if not (is_silent()) then show_open_subgoals_focused() +let print_subgoals () = if_verbose show_open_subgoals_focused () let _ = vinterp_add "SOLVE" |