From bb76b246d1396f788d18888abe8284befb7f44b9 Mon Sep 17 00:00:00 2001 From: filliatr Date: Tue, 3 Apr 2001 08:04:19 +0000 Subject: utilisation de Options.if_verbose git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1519 85f007b7-540e-0410-9357-904b9bb8a0f7 --- toplevel/vernacentries.ml | 40 ++++++++++++++++++---------------------- 1 file changed, 18 insertions(+), 22 deletions(-) (limited to 'toplevel/vernacentries.ml') 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" -- cgit v1.2.3