Getting rid of Pp.msg

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

7 files changed, 70 insertions, 69 deletions

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 7065bd265..b4e44e7d3 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -305,7 +305,6 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
 		else if Flags.is_auto_intros () then
 		  Pfedit.by (Refiner.tclDO len Tactics.intro);
 		(match tac with Some tac -> Pfedit.by tac | None -> ())) ();
-	       Flags.if_verbose (msg $$ Printer.pr_open_subgoals) ();
 	       id)
 	end)
 	
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 2256d1b1d..e13b80dc7 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -296,18 +296,16 @@ let cache_ml_module_object (_,{mnames=mnames}) =
        if not (module_is_known mname) then
 	 if has_dynlink then
            let fname = file_of_name mname in
+           let info = str"[Loading ML file " ++ str fname ++ str" ..." in
 	   try
-	     if_verbose
-	       msg (str"[Loading ML file " ++ str fname ++ str" ...");
              load_ml_object mname fname;
-             if_verbose msgnl (str" done]");
+             if_verbose msgnl (info ++ str" done]");
              add_loaded_module mname
            with e ->
-	     if_verbose msgnl (str" failed]");
+	     if_verbose msgnl (info ++ str" failed]");
 	     raise e
 	 else
-	     (if_verbose msgnl (str" failed]");
-	      error ("Dynamic link not supported (module "^name^")"))
+	      error ("Dynamic link not supported (module "^name^")")
        else init_ml_object mname)
     mnames
 
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 61cc6b348..5f07001ca 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -801,8 +801,7 @@ let rec solve_obligation prg num tac =
 	    trace (str "Started obligation " ++ int user_num ++ str "  proof: " ++
 		     Printer.pr_constr_env (Global.env ()) obl.obl_type);
 	    Pfedit.by (snd (get_default_tactic ()));
-	    Option.iter (fun tac -> Pfedit.set_end_tac (Tacinterp.interp tac)) tac;
-	    Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) ()
+	    Option.iter (fun tac -> Pfedit.set_end_tac (Tacinterp.interp tac)) tac
       | l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) "
 		      ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l))
 
diff --git a/toplevel/search.ml b/toplevel/search.ml
index e5b2ffbaf..fbfa83d08 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -24,6 +24,9 @@ open Libnames
 open Globnames
 open Nametab
 
+type filter_function = global_reference -> env -> constr -> bool
+type display_function = global_reference -> env -> constr -> unit
+
 module SearchBlacklist =
   Goptions.MakeStringTable
     (struct
@@ -107,10 +110,10 @@ let rec head c =
 
 let xor a b = (a or b) & (not (a & b))
 
-let plain_display ref a c =
+let plain_display accu ref a c =
   let pc = pr_lconstr_env a c in
   let pr = pr_global ref in
-  msg (hov 2 (pr ++ str":" ++ spc () ++ pc) ++ fnl ())
+  accu := !accu ++ hov 2 (pr ++ str":" ++ spc () ++ pc) ++ fnl ()
 
 let filter_by_module (module_list:dir_path list) (accept:bool)
   (ref:global_reference) _ _ =
@@ -193,14 +196,20 @@ let raw_search search_function extra_filter display_function pat =
 	 display_function gr env typ
     ) (search_function pat)
 
-let text_pattern_search extra_filter =
-  raw_search Libtypes.search_concl extra_filter plain_display
+let text_pattern_search extra_filter pat =
+  let ans = ref (mt ()) in
+  raw_search Libtypes.search_concl extra_filter (plain_display ans) pat;
+  !ans
 
-let text_search_rewrite extra_filter =
-  raw_search (Libtypes.search_eq_concl c_eq) extra_filter plain_display
+let text_search_rewrite extra_filter pat =
+  let ans = ref (mt ()) in
+  raw_search (Libtypes.search_eq_concl c_eq) extra_filter (plain_display ans) pat;
+  !ans
 
-let text_search_by_head extra_filter =
-  raw_search Libtypes.search_head_concl extra_filter plain_display
+let text_search_by_head extra_filter pat =
+  let ans = ref (mt ()) in
+  raw_search Libtypes.search_head_concl extra_filter (plain_display ans) pat;
+  !ans
 
 let filter_by_module_from_list = function
   | [], _ -> (fun _ _ _ -> true)
@@ -244,5 +253,7 @@ let raw_search_about filter_modules display_function l =
   in
   gen_filtered_search filter display_function
 
-let search_about ref inout =
-  raw_search_about (filter_by_module_from_list inout) plain_display ref
+let search_about reference inout =
+  let ans = ref (mt ()) in
+  raw_search_about (filter_by_module_from_list inout) (plain_display ans) reference;
+  !ans
diff --git a/toplevel/search.mli b/toplevel/search.mli
index d248a9faa..daca39f66 100644
--- a/toplevel/search.mli
+++ b/toplevel/search.mli
@@ -20,33 +20,28 @@ type glob_search_about_item =
   | GlobSearchSubPattern of constr_pattern
   | GlobSearchString of string
 
-val search_by_head : constr -> dir_path list * bool -> unit
-val search_rewrite : constr -> dir_path list * bool -> unit
-val search_pattern : constr -> dir_path list * bool -> unit
+type filter_function = global_reference -> env -> constr -> bool
+type display_function = global_reference -> env -> constr -> unit
+
+val search_by_head : constr -> dir_path list * bool -> std_ppcmds
+val search_rewrite : constr -> dir_path list * bool -> std_ppcmds
+val search_pattern : constr -> dir_path list * bool -> std_ppcmds
 val search_about  :
-  (bool * glob_search_about_item) list -> dir_path list * bool -> unit
+  (bool * glob_search_about_item) list -> dir_path list * bool -> std_ppcmds
 
 (** The filtering function that is by standard search facilities.
    It can be passed as argument to the raw search functions.
    It is used in pcoq. *)
 
-val filter_by_module_from_list :
-  dir_path list * bool -> global_reference -> env -> 'a -> bool
+val filter_by_module_from_list : dir_path list * bool -> filter_function
 
-val filter_blacklist : global_reference -> env -> constr -> bool
+val filter_blacklist : filter_function
 
 (** raw search functions can be used for various extensions.
    They are also used for pcoq. *)
-val gen_filtered_search : (global_reference -> env -> constr -> bool) ->
-      (global_reference -> env -> constr -> unit) -> unit
-val filtered_search : (global_reference -> env -> constr -> bool) ->
-  (global_reference -> env -> constr -> unit) -> global_reference -> unit
-val raw_pattern_search : (global_reference -> env -> constr -> bool) ->
-  (global_reference -> env -> constr -> unit) -> constr_pattern -> unit
-val raw_search_rewrite : (global_reference -> env -> constr -> bool) ->
-  (global_reference -> env -> constr -> unit) -> constr_pattern -> unit
-val raw_search_about : (global_reference -> env -> constr -> bool) ->
-  (global_reference -> env -> constr -> unit) ->
-      (bool * glob_search_about_item) list -> unit
-val raw_search_by_head : (global_reference -> env -> constr -> bool) ->
-  (global_reference -> env -> constr -> unit) -> constr_pattern -> unit
+val gen_filtered_search : filter_function -> display_function -> unit
+val filtered_search : filter_function -> display_function -> global_reference -> unit
+val raw_pattern_search : filter_function -> display_function -> constr_pattern -> unit
+val raw_search_rewrite : filter_function -> display_function -> constr_pattern -> unit
+val raw_search_about : filter_function -> display_function -> (bool * glob_search_about_item) list -> unit
+val raw_search_by_head : filter_function -> display_function -> constr_pattern -> unit
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 8aaa82a3b..6d37e0d78 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -192,7 +192,7 @@ let pr_new_syntax loc ocom =
     | Some com -> pr_vernac com
     | None -> mt() in
   if !beautify_file then
-    msg (hov 0 (comment (fst loc) ++ com ++ comment (snd loc)))
+    pp (hov 0 (comment (fst loc) ++ com ++ comment (snd loc)))
   else
     msgnl (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com)));
   States.unfreeze fs;
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index dd8f1cd0e..db3877dff 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -91,8 +91,7 @@ let show_top_evars () =
   let pfts = get_pftreestate () in
   let gls = Proof.V82.subgoals pfts in
   let sigma = gls.Evd.sigma in
-  msg (pr_evars_int 1 (Evarutil.non_instantiated sigma))
-  
+  msg_info (pr_evars_int 1 (Evarutil.non_instantiated sigma))
 
 let show_prooftree () =
   (* Spiwack: proof tree is currently not working *)
@@ -102,7 +101,7 @@ let enable_goal_printing = ref true
 
 let print_subgoals () =
   if !enable_goal_printing && is_verbose ()
-  then msg (pr_open_subgoals ())
+  then msg_info (pr_open_subgoals ())
 
 let try_print_subgoals () =
   Pp.flush_all();
@@ -164,7 +163,7 @@ let show_match id =
   let pr_branch l =
     str "| " ++ hov 1 (prlist_with_sep spc str l) ++ str " =>"
   in
-  msg (v 1 (str "match # with" ++ fnl () ++
+  msg_info (v 1 (str "match # with" ++ fnl () ++
 	    prlist_with_sep fnl pr_branch patterns ++ fnl ()))
 
 (* "Print" commands *)
@@ -380,7 +379,7 @@ let vernac_end_proof = function
     admit ()
   | Proved (is_opaque,idopt) ->
     let prf = Pfedit.get_current_proof_name () in
-    if is_verbose () && !qed_display_script then (show_script (); msg (fnl()));
+    if is_verbose () && !qed_display_script then show_script ();
     begin match idopt with
     | None -> save_named is_opaque
     | Some ((_,id),None) -> save_anonymous is_opaque id
@@ -1204,13 +1203,13 @@ let vernac_check_may_eval redexp glopt rc =
   match redexp with
     | None ->
 	if !pcoq <> None then (Option.get !pcoq).print_check env j
-	else msg (print_judgment env j)
+	else msg_info (print_judgment env j)
     | Some r ->
         let (sigma',r_interp) = interp_redexp env sigma' r in
 	let redfun = fst (reduction_of_red_expr r_interp) in
 	if !pcoq <> None
 	then (Option.get !pcoq).print_eval redfun env sigma' rc j
-	else msg (print_eval redfun env sigma' rc j)
+	else msg_info (print_eval redfun env sigma' rc j)
 
 let vernac_declare_reduction locality s r =
   declare_red_expr locality s (snd (interp_redexp (Global.env()) Evd.empty r))
@@ -1222,23 +1221,23 @@ let vernac_global_check c =
   let c = interp_constr evmap env c in
   let senv = Global.safe_env() in
   let j = Safe_typing.typing senv c in
-  msg (print_safe_judgment env j)
+  msg_info (print_safe_judgment env j)
 
 let vernac_print = function
-  | PrintTables -> print_tables ()
-  | PrintFullContext-> msg (print_full_context_typ ())
-  | PrintSectionContext qid -> msg (print_sec_context_typ qid)
-  | PrintInspect n -> msg (inspect n)
+  | PrintTables -> msg_info (print_tables ())
+  | PrintFullContext-> msg_info (print_full_context_typ ())
+  | PrintSectionContext qid -> msg_info (print_sec_context_typ qid)
+  | PrintInspect n -> msg_info (inspect n)
   | PrintGrammar ent -> Metasyntax.print_grammar ent
   | PrintLoadPath dir -> (* For compatibility ? *) print_loadpath dir
-  | PrintModules -> msg (print_modules ())
+  | PrintModules -> msg_info (print_modules ())
   | PrintModule qid -> print_module qid
   | PrintModuleType qid -> print_modtype qid
   | PrintMLLoadPath -> Mltop.print_ml_path ()
   | PrintMLModules -> Mltop.print_ml_modules ()
   | PrintName qid ->
       if !pcoq <> None then (Option.get !pcoq).print_name qid
-      else msg (print_name qid)
+      else msg_info (print_name qid)
   | PrintGraph -> ppnl (Prettyp.print_graph())
   | PrintClasses -> ppnl (Prettyp.print_classes())
   | PrintTypeClasses -> ppnl (Prettyp.print_typeclasses())
@@ -1253,25 +1252,25 @@ let vernac_print = function
     let univ = if b then Univ.sort_universes univ else univ in
     pp (Univ.pr_universes univ)
   | PrintUniverses (b, Some s) -> dump_universes b s
-  | PrintHint r -> Auto.print_hint_ref (smart_global r)
-  | PrintHintGoal -> Auto.print_applicable_hint ()
-  | PrintHintDbName s -> Auto.print_hint_db_by_name s
+  | PrintHint r -> msg_info (Auto.pr_hint_ref (smart_global r))
+  | PrintHintGoal -> msg_info (Auto.pr_applicable_hint ())
+  | PrintHintDbName s -> msg_info (Auto.pr_hint_db_by_name s)
   | PrintRewriteHintDbName s -> Autorewrite.print_rewrite_hintdb s
-  | PrintHintDb -> Auto.print_searchtable ()
+  | PrintHintDb -> msg_info (Auto.pr_searchtable ())
   | PrintScopes ->
       pp (Notation.pr_scopes (Constrextern.without_symbols pr_lglob_constr))
   | PrintScope s ->
       pp (Notation.pr_scope (Constrextern.without_symbols pr_lglob_constr) s)
   | PrintVisibility s ->
       pp (Notation.pr_visibility (Constrextern.without_symbols pr_lglob_constr) s)
-  | PrintAbout qid -> msg (print_about qid)
-  | PrintImplicit qid -> msg (print_impargs qid)
+  | PrintAbout qid -> msg_info (print_about qid)
+  | PrintImplicit qid -> msg_info (print_impargs qid)
   | PrintAssumptions (o,r) ->
       (* Prints all the axioms and section variables used by a term *)
       let cstr = constr_of_global (smart_global r) in
       let st = Conv_oracle.get_transp_state () in
       let nassums = Assumptions.assumptions st ~add_opaque:o cstr in
-      msg (Printer.pr_assumptionset (Global.env ()) nassums)
+      msg_info (Printer.pr_assumptionset (Global.env ()) nassums)
 
 let global_module r =
   let (loc,qid) = qualid_of_reference r in
@@ -1310,15 +1309,15 @@ let vernac_search s r =
   match s with
   | SearchPattern c ->
       let (_,c) = interp_open_constr_patvar Evd.empty (Global.env()) c in
-      Search.search_pattern c r
+      msg_info (Search.search_pattern c r)
   | SearchRewrite c ->
       let _,pat = interp_open_constr_patvar Evd.empty (Global.env()) c in
-      Search.search_rewrite pat r
+      msg_info (Search.search_rewrite pat r)
   | SearchHead c ->
       let _,pat = interp_open_constr_patvar Evd.empty (Global.env()) c in
-      Search.search_by_head pat r
+      msg_info (Search.search_by_head pat r)
   | SearchAbout sl ->
-      Search.search_about (List.map (on_snd interp_search_about_item) sl) r
+      msg_info (Search.search_about (List.map (on_snd interp_search_about_item) sl) r)
 
 let vernac_locate = function
   | LocateTerm (AN qid) -> msgnl (print_located_qualid qid)
@@ -1420,7 +1419,7 @@ let vernac_unfocus () =
 let vernac_unfocused () =
   let p = Proof_global.give_me_the_proof () in
   if Proof.unfocused p then
-    msg (str"The proof is indeed fully unfocused.")
+    msg_info (str"The proof is indeed fully unfocused.")
   else
     error "The proof is not fully unfocused."
 
@@ -1458,14 +1457,14 @@ let vernac_bullet (bullet:Proof_global.Bullet.t) =
 let vernac_show = function
   | ShowGoal goalref ->
       if !pcoq <> None then (Option.get !pcoq).show_goal goalref
-      else msg (match goalref with
+      else msg_info (match goalref with
 	| OpenSubgoals -> pr_open_subgoals ()
 	| NthGoal n -> pr_nth_open_subgoal n
         | GoalId id -> pr_goal_by_id id)
   | ShowGoalImplicitly None ->
-      Constrextern.with_implicits msg (pr_open_subgoals ())
+      Constrextern.with_implicits msg_info (pr_open_subgoals ())
   | ShowGoalImplicitly (Some n) ->
-      Constrextern.with_implicits msg (pr_nth_open_subgoal n)
+      Constrextern.with_implicits msg_info (pr_nth_open_subgoal n)
   | ShowProof -> show_proof ()
   | ShowNode -> show_node ()
   | ShowScript -> show_script ()