[toplevel] [emacs] Don't quote errors in emacs mode.

In 8.6 + emacs, errors were quoted sometimes with special
markers (e.g. `Print Module foo.` for a non-existing `foo`)

In 8.7 we uniformized error handling and now all errors are quoted,
however, this behavior confuses emacs as it seems that the quotes are
meant to be applied only to warnings.

We thus reflect the de-facto situation, removing quoting for errors
and updating the code so it is clear that the quoter is a warnings
quoter. We also update the warnings quoter to use a warning tag
instead of a non-printable char.

This fixes ProofGeneral for trunk users.

c.f. https://github.com/ProofGeneral/PG/issues/175

1 files changed, 12 insertions, 15 deletions

diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index a4acd3f24..c25dd55fb 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -112,26 +112,23 @@ let msgnl_with ?pre_hdr fmt strm =
   pp_with fmt (strm ++ fnl ());
   Format.pp_print_flush fmt ()
 
-(* XXX: This is really painful! *)
 module Emacs = struct
 
   (* Special chars for emacs, to detect warnings inside goal output *)
-  let emacs_quote_start = String.make 1 (Char.chr 254)
-  let emacs_quote_end   = String.make 1 (Char.chr 255)
+  let quote_warning_start = "<warning>"
+  let quote_warning_end = "</warning>"
 
-  let emacs_quote_err g =
-    hov 0 (str emacs_quote_start ++ g ++ str emacs_quote_end)
+  let quote_info_start = "<infomsg>"
+  let quote_info_end = "</infomsg>"
 
-  let emacs_quote_info_start = "<infomsg>"
-  let emacs_quote_info_end = "</infomsg>"
+  let quote_emacs q_start q_end msg =
+    hov 0 (seq [str q_start; brk(0,0); msg; brk(0,0); str q_end])
 
-  let emacs_quote_info g =
-    hov 0 (str emacs_quote_info_start++ brk(0,0) ++ g ++ brk(0,0) ++ str emacs_quote_info_end)
+  let quote_warning = quote_emacs quote_warning_start quote_warning_end
+  let quote_info = quote_emacs quote_info_start quote_info_end
 
 end
 
-open Emacs
-
 let  dbg_hdr = tag Tag.debug   (str "Debug:")   ++ spc ()
 let info_hdr = mt ()
 let warn_hdr = tag Tag.warning (str "Warning:") ++ spc ()
@@ -144,13 +141,13 @@ let make_body quoter info ?pre_hdr s =
 (* The empty quoter *)
 let noq x = x
 (* Generic logger *)
-let gen_logger dbg err ?pre_hdr level msg = match level with
+let gen_logger dbg warn ?pre_hdr level msg = match level with
   | Debug   -> msgnl_with !std_ft (make_body dbg  dbg_hdr ?pre_hdr msg)
   | Info    -> msgnl_with !std_ft (make_body dbg info_hdr ?pre_hdr msg)
   | Notice  -> msgnl_with !std_ft (make_body noq info_hdr ?pre_hdr msg)
   | Warning -> Flags.if_warn (fun () ->
-               msgnl_with !err_ft (make_body err warn_hdr ?pre_hdr msg)) ()
-  | Error   -> msgnl_with !err_ft (make_body err  err_hdr ?pre_hdr msg)
+               msgnl_with !err_ft (make_body warn warn_hdr ?pre_hdr msg)) ()
+  | Error   -> msgnl_with !err_ft (make_body noq   err_hdr ?pre_hdr msg)
 
 (** Standard loggers *)
 
@@ -261,7 +258,7 @@ let init_color_output () =
    - Warning/Error: emacs_quote_err
    - Notice: unquoted
  *)
-let emacs_logger = gen_logger emacs_quote_info emacs_quote_err
+let emacs_logger = gen_logger Emacs.quote_info Emacs.quote_warning
 
 (* Output to file, used only in extraction so a candidate for removal *)
 let ft_logger old_logger ft ?loc level mesg =