Fixing info_auto / info_trivial display.

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

2 files changed, 13 insertions, 14 deletions

diff --git a/lib/pp.ml4 b/lib/pp.ml4
index 4eaf96263..d05abbcd0 100644
--- a/lib/pp.ml4
+++ b/lib/pp.ml4
@@ -346,7 +346,7 @@ let print_color s x =
 let make_body color info s =
   emacs_quote (print_color color (print_color "1" (hov 0 (info ++ spc () ++ s))))
 
-let debugbody strm = print_color "36" (str "Debug:" ++ spc () ++ strm) (* cyan *)
+let debugbody strm = print_color "36" (hov 0 (str "Debug:" ++ spc () ++ strm)) (* cyan *)
 let warnbody strm = make_body "93" (str "Warning:") strm (* bright yellow *)
 let errorbody strm = make_body "31" (str "Error:") strm (* bright red *)
 
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 0486eec58..812ebd206 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -1207,33 +1207,32 @@ and erase_subtree depth = function
   | (d,_) :: l -> if d = depth then l else erase_subtree depth l
 
 let pr_info_atom (d,pp) =
-  msg_debug (str (String.make d ' ') ++ pp () ++ str ".")
+  str (String.make d ' ') ++ pp () ++ str "."
 
 let pr_info_trace = function
   | (Info,_,{contents=(d,Some pp)::l}) ->
-      List.iter pr_info_atom (cleanup_info_trace d [(d,pp)] l)
-  | _ -> ()
+      prlist_with_sep fnl pr_info_atom (cleanup_info_trace d [(d,pp)] l)
+  | _ -> mt ()
 
 let pr_info_nop = function
-  | (Info,_,_) -> msg_debug (str "idtac.")
-  | _ -> ()
+  | (Info,_,_) -> str "idtac."
+  | _ -> mt ()
 
 let pr_dbg_header = function
-  | (Off,_,_) -> ()
-  | (Debug,0,_) -> msg_debug (str "(* debug trivial : *)")
-  | (Debug,_,_) -> msg_debug (str "(* debug auto : *)")
-  | (Info,0,_) -> msg_debug (str "(* info trivial : *)")
-  | (Info,_,_) -> msg_debug (str "(* info auto : *)")
+  | (Off,_,_) -> mt ()
+  | (Debug,0,_) -> str "(* debug trivial : *)"
+  | (Debug,_,_) -> str "(* debug auto : *)"
+  | (Info,0,_) -> str "(* info trivial : *)"
+  | (Info,_,_) -> str "(* info auto : *)"
 
 let tclTRY_dbg d tac =
   tclORELSE0
     (fun gl ->
-      pr_dbg_header d;
       let out = tac gl in
-      pr_info_trace d;
+      msg_debug (pr_dbg_header d ++ fnl () ++ pr_info_trace d);
       out)
     (fun gl ->
-      pr_info_nop d;
+      msg_debug (pr_info_nop d);
       tclIDTAC gl)
 
 (**************************************************************************)