msg_info now puts infomsg tag in emacs mode.

Fixes the idtac "string" not appearing in proofgeneral because
printined *before* the goal.

2 files changed, 12 insertions, 4 deletions

diff --git a/lib/pp.ml b/lib/pp.ml
index 81a19d86de..fa21506b33 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -370,10 +370,17 @@ let pp_dirs ?pp_tag ft =
 let emacs_quote_start = String.make 1 (Char.chr 254)
 let emacs_quote_end = String.make 1 (Char.chr 255)
 
+let emacs_quote_info_start = "<infomsg>"
+let emacs_quote_info_end = "</infomsg>"
+
 let emacs_quote g =
   if !print_emacs then str emacs_quote_start ++ hov 0 g ++ str emacs_quote_end
   else hov 0 g
 
+let emacs_quote_info g =
+  if !print_emacs then str emacs_quote_info_start ++ hov 0 g ++ str emacs_quote_info_end
+  else hov 0 g
+
 
 (* pretty printing functions WITHOUT FLUSH *)
 let pp_with ?pp_tag ft strm =
@@ -434,10 +441,11 @@ let make_body info s =
 let debugbody strm = hov 0 (str "Debug:" ++ spc () ++ strm)
 let warnbody strm = make_body (str "Warning:") strm
 let errorbody strm = make_body (str "Error:") strm
+let infobody strm = emacs_quote_info strm
 
 let std_logger ~id:_ level msg = match level with
 | Debug _ -> msgnl (debugbody msg)
-| Info -> msgnl (hov 0 msg)
+| Info -> msgnl (infobody (hov 0 msg))
 | Notice -> msgnl msg
 | Warning -> Flags.if_warn (fun () -> msgnl_with !err_ft (warnbody msg)) ()
 | Error -> msgnl_with !err_ft (errorbody msg)
diff --git a/lib/pp.mli b/lib/pp.mli
index d4314a3366..9f65c0be0b 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -124,9 +124,9 @@ type logger = message_level -> std_ppcmds -> unit
 
 (** {6 output functions}
 
-[msg_info] and [msg_notice] do not put any decoration on output by
-default. If possible don't mix them with goal output (prefer
-msg_warning) so that dispatching of outputs is easier. Once all
+[msg_notice] do not put any decoration on output by default. If
+possible don't mix it with goal output (prefer msg_info or
+msg_warning) so that interfaces can dispatch outputs easily. Once all
 interfaces use the xml-like protocol this constraint can be
 relaxed. *)
 (* Should we advertise these functions more? Should they be the ONLY