Getting rid of Pp.msg

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

28 files changed, 179 insertions, 177 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 3194b2681..5b8507304 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -106,7 +106,8 @@ let check_one_lib admit (dir,m) =
     (Flags.if_verbose msgnl
       (str "Checking library: " ++ pr_dirpath dir);
       Safe_typing.import file md dig);
-  Flags.if_verbose msg(fnl());
+  Flags.if_verbose pp (fnl());
+  pp_flush ();
   register_loaded_library m
 
 (*************************************************************************)
@@ -287,7 +288,7 @@ let name_clash_message dir mdir f =
 let depgraph = ref LibraryMap.empty
 
 let intern_from_file (dir, f) =
-  Flags.if_verbose msg (str"[intern "++str f++str" ...");
+  Flags.if_verbose pp (str"[intern "++str f++str" ..."); pp_flush ();
   let (md,table,digest) =
     try
       let ch = with_magic_number_check raw_intern_library f in
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 2a2833caa..b3ede70bf 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -222,7 +222,7 @@ let constr_display csr =
     | Anonymous -> "Anonymous"
 
   in
-    msg (str (term_display csr) ++fnl ())
+  Pp.pp (str (term_display csr) ++fnl ()); Pp.pp_flush ()
 
 open Format;;
 
diff --git a/lib/pp.ml4 b/lib/pp.ml4
index 0a3466859..35621a5d7 100644
--- a/lib/pp.ml4
+++ b/lib/pp.ml4
@@ -327,6 +327,7 @@ let flush_all() = flush stderr; flush stdout; pp_flush()
 (* pretty printing functions WITH FLUSH *)
 let msg x = msg_with !std_ft x
 let msgnl x = msgnl_with !std_ft x
+let msg_info x = msgnl x
 let msgerr x = msg_with !err_ft x
 let msgerrnl x = msgnl_with !err_ft x
 let msg_warning x = msg_warning_with !err_ft x
diff --git a/lib/pp.mli b/lib/pp.mli
index da37a1153..135343092 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -96,6 +96,9 @@ val msgnl_with : Format.formatter -> std_ppcmds -> unit
 
 (** {6 Pretty-printing functions {% \emph{%}without flush{% }%} on [stdout] and [stderr]. } *)
 
+(** These functions are low-level interace to printing and should not be used
+    in usual code. Consider using the [msg_*] function family instead. *)
+
 val pp : std_ppcmds -> unit
 val ppnl : std_ppcmds -> unit
 val pperr : std_ppcmds -> unit
@@ -104,19 +107,22 @@ val message : string -> unit       (** = pPNL *)
 val pp_flush : unit -> unit
 val flush_all: unit -> unit
 
-(** {6 Pretty-printing functions {% \emph{%}with flush{% }%} on [stdout] and [stderr]. } *)
+(** {6 Sending messages to the user } *)
 
-val msg : std_ppcmds -> unit
-val msgnl : std_ppcmds -> unit
-val msgerr : std_ppcmds -> unit
-val msgerrnl : std_ppcmds -> unit
+val msg_info : std_ppcmds -> unit
 val msg_warning : std_ppcmds -> unit
-
-(** Same specific display in emacs as warning, but without the "Warning:" **)
 val msg_debug : std_ppcmds -> unit
 
 val string_of_ppcmds : std_ppcmds -> string
 
+(** {6 Deprecated functions} *)
+
+(** DEPRECATED. Do not use in newly written code. *)
+val msg : std_ppcmds -> unit
+val msgnl : std_ppcmds -> unit
+val msgerr : std_ppcmds -> unit
+val msgerrnl : std_ppcmds -> unit
+
 (** {6 Location management. } *)
 
 type loc = Loc.t
diff --git a/library/goptions.ml b/library/goptions.ml
index 1a490c8ce..47aa401b6 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -106,7 +106,7 @@ module MakeTable =
          (fun c -> t := MySet.remove c !t))
 
     let print_table table_name printer table =
-      msg (str table_name ++
+      pp (str table_name ++
 	   (hov 0
 	      (if MySet.is_empty table then str "None" ++ fnl ()
                else MySet.fold
@@ -120,7 +120,7 @@ module MakeTable =
       method mem x =
 	let y = A.encode x in
         let answer = MySet.mem y !t in
-        msg (A.member_message y answer ++ fnl ())
+        msg_info (A.member_message y answer)
       method print = print_table A.title A.printer !t
     end
 
@@ -354,11 +354,9 @@ let print_option_value key =
   let s = read () in
   match s with
     | BoolValue b ->
-	msg (str ("The "^name^" mode is "^(if b then "on" else "off")) ++
-	     fnl ())
+	msg_info (str ("The "^name^" mode is "^(if b then "on" else "off")))
     | _ ->
-	msg (str ("Current value of "^name^" is ") ++
-	     msg_option_value (name,s) ++ fnl ())
+	msg_info (str ("Current value of "^name^" is ") ++ msg_option_value (name, s))
 
 
 let get_tables () =
@@ -380,27 +378,26 @@ let print_tables () =
     if depr then msg ++ str " [DEPRECATED]" ++ fnl ()
     else msg ++ fnl ()
   in
-  msg
-    (str "Synchronous options:" ++ fnl () ++
-     OptionMap.fold
-       (fun key (name, depr, (sync,read,_,_,_)) p ->
-	  if sync then p ++ print_option key name (read ()) depr
-	  else p)
-       !value_tab (mt ()) ++
-     str "Asynchronous options:" ++ fnl () ++
-     OptionMap.fold
-       (fun key (name, depr, (sync,read,_,_,_)) p ->
-	  if sync then p
-	  else p ++ print_option key name (read ()) depr)
-       !value_tab (mt ()) ++
-     str "Tables:" ++ fnl () ++
-     List.fold_right
-       (fun (nickkey,_) p -> p ++ str ("  "^nickkey) ++ fnl ())
-       !string_table (mt ()) ++
-     List.fold_right
-       (fun (nickkey,_) p -> p ++ str ("  "^nickkey) ++ fnl ())
-       !ref_table (mt ()) ++
-     fnl ()
-    )
+  str "Synchronous options:" ++ fnl () ++
+    OptionMap.fold
+      (fun key (name, depr, (sync,read,_,_,_)) p ->
+        if sync then p ++ print_option key name (read ()) depr
+        else p)
+      !value_tab (mt ()) ++
+  str "Asynchronous options:" ++ fnl () ++
+    OptionMap.fold
+      (fun key (name, depr, (sync,read,_,_,_)) p ->
+        if sync then p
+        else p ++ print_option key name (read ()) depr)
+      !value_tab (mt ()) ++
+  str "Tables:" ++ fnl () ++
+    List.fold_right
+      (fun (nickkey,_) p -> p ++ str ("  "^nickkey) ++ fnl ())
+      !string_table (mt ()) ++
+    List.fold_right
+      (fun (nickkey,_) p -> p ++ str ("  "^nickkey) ++ fnl ())
+      !ref_table (mt ()) ++
+    fnl ()
+
 
 
diff --git a/library/goptions.mli b/library/goptions.mli
index a90689dfc..29b6adb6e 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -164,6 +164,6 @@ val set_string_option_value : option_name -> string -> unit
 val print_option_value : option_name -> unit
 
 val get_tables : unit -> Interface.option_state OptionMap.t
-val print_tables : unit -> unit
+val print_tables : unit -> std_ppcmds
 
 val error_undeclared_key : option_name -> 'a
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 7434f5e8a..699f1f3df 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -696,14 +696,15 @@ type explanation =
 let check_disequalities state =
   let uf=state.uf in
   let rec check_aux = function
-      dis::q ->
-	debug (fun () -> msg
-	(str "Checking if " ++ pr_idx_term state dis.lhs ++ str " = " ++
-	 pr_idx_term state dis.rhs ++ str " ... ")) ();
-	if find uf dis.lhs=find uf dis.rhs then
-	  begin debug msgnl (str "Yes");Some dis end
-	else
-	  begin debug msgnl (str "No");check_aux q end
+    | dis::q ->
+        let (info, ans) =
+          if find uf dis.lhs = find uf dis.rhs then (str "Yes", Some dis)
+          else (str "No", check_aux q)
+        in
+        let _ = debug (fun () -> msg_debug
+        (str "Checking if " ++ pr_idx_term state dis.lhs ++ str " = " ++
+         pr_idx_term state dis.rhs ++ str " ... " ++ info)) () in
+        ans
     | [] -> None
   in
     check_aux state.diseq
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index 4438c5897..fe86e1ae1 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -99,7 +99,7 @@ END
 
 VERNAC COMMAND EXTEND PrintExtractionInline
 | [ "Print" "Extraction" "Inline" ]
-  -> [ print_extraction_inline () ]
+  -> [ msg_info (print_extraction_inline ()) ]
 END
 
 VERNAC COMMAND EXTEND ResetExtractionInline
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index ecedc9002..0efdbbb6b 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -606,7 +606,6 @@ let extraction_inline b l =
 let print_extraction_inline () =
   let (i,n)= !inline_table in
   let i'= Refset'.filter (function ConstRef _ -> true | _ -> false) i in
-  msg
     (str "Extraction Inline:" ++ fnl () ++
      Refset'.fold
        (fun r p ->
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 7505664a6..978760e8e 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -177,7 +177,7 @@ val find_custom_match : ml_branch array -> string
 
 val extraction_language : lang -> unit
 val extraction_inline : bool -> reference list -> unit
-val print_extraction_inline : unit -> unit
+val print_extraction_inline : unit -> Pp.std_ppcmds
 val reset_extraction_inline : unit -> unit
 val extract_constant_inline :
   bool -> reference -> string list -> string -> unit
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index d1fc8ef33..a169c2826 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -16,10 +16,10 @@ let observe strm =
   if do_observe ()
   then Pp.msgnl strm
   else ()
-let observennl strm =
+(*let observennl strm =
   if do_observe ()
   then Pp.msg strm
-  else ()
+  else ()*)
 
 
 type binder_type =
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index b0897c61e..b463b6c27 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -55,10 +55,10 @@ let observe strm =
   then Pp.msgnl strm
   else ()
 
-let observennl strm =
+(*let observennl strm =
   if do_observe ()
   then begin Pp.msg strm;Pp.pp_flush () end
-  else ()
+  else ()*)
 
 
 let do_observe_tac s tac g =
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index d772279f1..a1ab6cd30 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -472,7 +472,7 @@ and pp_atom= function
   | Atom n -> int n
   | f -> str "(" ++ hv 2 (pp_form f) ++ str ")"
 
-let pr_form f = msg (pp_form f)
+let pr_form f = pp_form f
 
 let pp_intmap map =
   let pp=ref (str "") in
diff --git a/plugins/rtauto/proof_search.mli b/plugins/rtauto/proof_search.mli
index 275e94cde..738f3f230 100644
--- a/plugins/rtauto/proof_search.mli
+++ b/plugins/rtauto/proof_search.mli
@@ -40,7 +40,7 @@ val success: state -> bool
 
 val pp: state -> Pp.std_ppcmds
 
-val pr_form : form -> unit
+val pr_form : form -> Pp.std_ppcmds
 
 val reset_info : unit -> unit
 
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 783aebafd..a095c545f 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -128,10 +128,10 @@ TACTIC EXTEND closed_term
 END
 ;;
 
-TACTIC EXTEND echo
+(* TACTIC EXTEND echo
 | [ "echo" constr(t) ] ->
   [ Pp.msg (Termops.print_constr t);  Tacinterp.eval_tactic (TacId []) ]
-END;;
+END;;*)
 
 (*
 let closed_term_ast l =
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 221c46a92..cb588af2d 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -89,7 +89,7 @@ let tclIDTAC gls = goal_goal_list gls
 
 (* the message printing identity tactic *)
 let tclIDTAC_MESSAGE s gls =
-  msg (hov 0 s); tclIDTAC gls
+  pp (hov 0 s); pp_flush (); tclIDTAC gls
 
 (* General failure tactic *)
 let tclFAIL_s s gls = errorlabstrm "Refiner.tclFAIL_s" (str s)
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index b23f361c7..d09c7f05a 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -60,7 +60,7 @@ let help () =
 let goal_com g tac =
   begin
     db_pr_goal g;
-    msg (str "Going to execute:" ++ fnl () ++ !prtac tac ++ fnl ())
+    msgnl (str "Going to execute:" ++ fnl () ++ !prtac tac)
   end
 
 let skipped = ref 0
@@ -105,14 +105,14 @@ let run ini =
     for i=1 to 2 do
       print_char (Char.chr 8);print_char (Char.chr 13)
     done;
-    msg (str "Executed expressions: " ++ int !skipped ++ fnl() ++ fnl())
+    msgnl (str "Executed expressions: " ++ int !skipped ++ fnl())
   end;
   incr skipped
 
 (* Prints the prompt *)
 let rec prompt level =
   begin
-    msg (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ");
+    pp (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ");
     flush stdout;
     let exit () = skip:=0;skipped:=0;raise Sys.Break in
     let inst = try read_line () with End_of_file -> exit () in
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 404516279..96cef72b4 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -411,6 +411,10 @@ module Hint_db = struct
     f None (List.map (fun x -> snd (snd x)) db.hintdb_nopat);
     Constr_map.iter (fun k (l,l',_) -> f (Some k) (List.map snd (l@l'))) db.hintdb_map
 
+  let fold f db accu =
+    let accu = f None (List.map (fun x -> snd (snd x)) db.hintdb_nopat) accu in
+    Constr_map.fold (fun k (l,l',_) -> f (Some k) (List.map snd (l@l'))) db.hintdb_map accu
+
   let transparent_state db = db.hintdb_state
 
   let set_transparent_state db st =
@@ -921,7 +925,6 @@ let pr_hint_list_for_head c =
 let pr_hint_ref ref = pr_hint_list_for_head ref
 
 (* Print all hints associated to head id in any database *)
-let print_hint_ref ref =  ppnl(pr_hint_ref ref)
 
 let pr_hint_term cl =
   try
@@ -949,53 +952,51 @@ let pr_hint_term cl =
 let error_no_such_hint_database x =
   error ("No such Hint database: "^x^".")
 
-let print_hint_term cl = ppnl (pr_hint_term cl)
-
 (* print all hints that apply to the concl of the current goal *)
-let print_applicable_hint () =
+let pr_applicable_hint () =
   let pts = get_pftreestate () in
   let glss = Proof.V82.subgoals pts in
   match glss.Evd.it with
   | [] -> Errors.error "No focused goal."
   | g::_ ->
     let gl = { Evd.it = g; sigma = glss.Evd.sigma } in
-    print_hint_term (pf_concl gl)
+    pr_hint_term (pf_concl gl)
 
 (* displays the whole hint database db *)
-let print_hint_db db =
+let pr_hint_db db =
+  let content =
+    let fold head hintlist accu =
+      let goal_descr = match head with
+      | None -> str "For any goal"
+      | Some head -> str "For " ++ pr_global head
+      in
+      let hints = pr_hint_list (List.map (fun x -> (0, x)) hintlist) in
+      let hint_descr = hov 0 (goal_descr ++ str " -> " ++ hints) in
+      accu ++ hint_descr
+    in
+    Hint_db.fold fold db (mt ())
+  in
   let (ids, csts) = Hint_db.transparent_state db in
-  msgnl (hov 0
-	  ((if Hint_db.use_dn db then str"Discriminated database"
-	    else str"Non-discriminated database")));
-  msgnl (hov 2 (str"Unfoldable variable definitions: " ++ pr_idpred ids));
-  msgnl (hov 2 (str"Unfoldable constant definitions: " ++ pr_cpred csts));
-  msgnl (hov 2 (str"Cut: " ++ pp_hints_path (Hint_db.cut db)));
-  Hint_db.iter
-    (fun head hintlist ->
-      match head with
-      | Some head ->
-	  msg (hov 0
-		  (str "For " ++ pr_global head ++ str " -> " ++
-		      pr_hint_list (List.map (fun x -> (0,x)) hintlist)))
-      | None ->
-	  msg (hov 0
-		  (str "For any goal -> " ++
-		      pr_hint_list (List.map (fun x -> (0, x)) hintlist))))
-    db
-
-let print_hint_db_by_name dbname =
+  hov 0
+    ((if Hint_db.use_dn db then str"Discriminated database"
+      else str"Non-discriminated database")) ++ fnl () ++
+  hov 2 (str"Unfoldable variable definitions: " ++ pr_idpred ids) ++ fnl () ++
+  hov 2 (str"Unfoldable constant definitions: " ++ pr_cpred csts) ++ fnl () ++
+  hov 2 (str"Cut: " ++ pp_hints_path (Hint_db.cut db)) ++ fnl () ++
+  content
+
+let pr_hint_db_by_name dbname =
   try
-    let db = searchtable_map dbname in print_hint_db db
+    let db = searchtable_map dbname in pr_hint_db db
   with Not_found ->
     error_no_such_hint_database dbname
 
 (* displays all the hints of all databases *)
-let print_searchtable () =
-  Hintdbmap.iter
-    (fun name db ->
-       msg (str "In the database " ++ str name ++ str ":" ++ fnl ());
-       print_hint_db db)
-    !searchtable
+let pr_searchtable () =
+  let fold name db accu =
+    str "In the database " ++ str name ++ str ":" ++ fnl () ++ pr_hint_db db
+  in
+  Hintdbmap.fold fold !searchtable (mt ())
 
 (**************************************************************************)
 (*                           Automatic tactics                            *)
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 67e4dac97..792900984 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -19,6 +19,7 @@ open Globnames
 open Vernacexpr
 open Mod_subst
 open Misctypes
+open Pp
 
 (** Auto and related automation tactics *)
 
@@ -124,15 +125,11 @@ val add_hints : locality_flag -> hint_db_name list -> hints_entry -> unit
 
 val prepare_hint : env -> open_constr -> constr
 
-val print_searchtable : unit -> unit
-
-val print_applicable_hint : unit -> unit
-
-val print_hint_ref : global_reference -> unit
-
-val print_hint_db_by_name : hint_db_name -> unit
-
-val print_hint_db : Hint_db.t -> unit
+val pr_searchtable : unit -> std_ppcmds
+val pr_applicable_hint : unit -> std_ppcmds
+val pr_hint_ref : global_reference -> std_ppcmds
+val pr_hint_db_by_name : hint_db_name -> std_ppcmds
+val pr_hint_db : Hint_db.t -> std_ppcmds
 
 (** [make_exact_entry pri (c, ctyp)].
    [c] is the term given as an exact proof to solve the goal;
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 82b08289d..cdb192ffa 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -779,6 +779,5 @@ END
 VERNAC COMMAND EXTEND GrabEvars
 [ "Grab" "Existential" "Variables" ] ->
   [ let p = Proof_global.give_me_the_proof () in
-    Proof.V82.grab_evars p;
-    Flags.if_verbose (fun () -> Pp.msg (Printer.pr_open_subgoals ())) () ]
+    Proof.V82.grab_evars p ]
 END
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 16eb595ea..665ab5b39 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1742,8 +1742,7 @@ let add_morphism_infer glob m n =
 				   glob (ConstRef cst));
 		  declare_projection n instance_id (ConstRef cst)
 		| _ -> assert false);
-	    Pfedit.by (Tacinterp.interp <:tactic< Coq.Classes.SetoidTactics.add_morphism_tactic>>)) ();
-	Flags.if_verbose (fun x -> msg (Printer.pr_open_subgoals x)) ()
+	    Pfedit.by (Tacinterp.interp <:tactic< Coq.Classes.SetoidTactics.add_morphism_tactic>>)) ()
 
 let add_morphism glob binders m s n =
   init_setoid ();
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 ()