utilisation de Options.if_verbose

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1519 85f007b7-540e-0410-9357-904b9bb8a0f7

11 files changed, 46 insertions, 46 deletions

diff --git a/contrib/extraction/Extraction.v b/contrib/extraction/Extraction.v
index a5ec0a693..1f71ef2f2 100644
--- a/contrib/extraction/Extraction.v
+++ b/contrib/extraction/Extraction.v
@@ -11,7 +11,7 @@ Declare ML Module "mlutil.cmo" "ocaml.cmo" "extraction.cmo" "extract_env.cmo".
 Grammar vernac vernac : ast :=
   extr_constr [ "Extraction" constrarg($c) "." ] -> 
               [ (Extraction $c) ]
-| extr_list   [ "Extraction" "-r" ne_qualidarg_list($l) "." ] ->
+| extr_list   [ "Recursive" "Extraction" ne_qualidarg_list($l) "." ] ->
               [ (ExtractionRec ($LIST $l)) ]
 | extr_list   [ "Extraction" stringarg($f) ne_qualidarg_list($l) "." ] ->
               [ (ExtractionFile $f ($LIST $l)) ]
diff --git a/lib/options.ml b/lib/options.ml
index 82ee767d3..52babfdb2 100644
--- a/lib/options.ml
+++ b/lib/options.ml
@@ -35,6 +35,9 @@ let silently f x =
     silent := oldsilent; raise e
   end
 
+let if_silent f x = if !silent then f x
+let if_verbose f x = if not !silent then f x
+
 (* The number of printed hypothesis in a goal *)
 
 let print_hyps_limit = ref (None : int option)
diff --git a/lib/options.mli b/lib/options.mli
index 61372bfe5..8d1d7e2fd 100644
--- a/lib/options.mli
+++ b/lib/options.mli
@@ -21,6 +21,8 @@ val make_silent : bool -> unit
 val is_silent : unit -> bool
 val is_verbose : unit -> bool
 val silently : ('a -> 'b) -> 'a -> 'b
+val if_silent : ('a -> unit) -> 'a -> unit
+val if_verbose : ('a -> unit) -> 'a -> unit
 
 val set_print_hyps_limit : int -> unit
 val unset_print_hyps_limit : unit -> unit
diff --git a/library/declare.ml b/library/declare.ml
index 9cd104121..59828c3cc 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -480,7 +480,7 @@ let declare_one_elimination mispec =
     let _ = declare_constant (id_of_string na)
       (ConstantEntry { const_entry_body = c; const_entry_type = None }, 
        NeverDischarge,false) in
-    if Options.is_verbose() then pPNL [< 'sTR na; 'sTR " is defined" >]
+    Options.if_verbose pPNL [< 'sTR na; 'sTR " is defined" >]
   in
   let env = Global.env () in
   let sigma = Evd.empty in
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index c422b0069..b5f4d88f0 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -1189,5 +1189,5 @@ let add_tacdef na vbody =
          "There is already a Meta Definition or a Tactic Definition named ";
          'sTR na>];
     let _ = Lib.add_leaf (id_of_string na) OBJ (inMD (na,vbody)) in
-    if Options.is_verbose() then mSGNL [< 'sTR (na ^ " is defined") >]
+    Options.if_verbose mSGNL [< 'sTR (na ^ " is defined") >]
   end
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"