Update behavior of -emacs to support showing diffs in ProofGeneral (master branch)

Adds XML-like tags in output to mark diffs

2 files changed, 15 insertions, 2 deletions

diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index 60b0bdc7e7..7bc3264968 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -196,6 +196,18 @@ let init_tag_map styles =
 let default_styles () =
   init_tag_map (default_tag_map ())
 
+let set_emacs_print_strings () =
+  let open Terminal in
+  let diff = "diff." in
+  List.iter (fun b ->
+      let (name, attrs) = b in
+      if diff = (String.sub name 0 (String.length diff)) then
+        tag_map := CString.Map.add name
+          { attrs with prefix = Some (Printf.sprintf "<%s>" name);
+                       suffix = Some (Printf.sprintf "</%s>" name) }
+          !tag_map)
+    (CString.Map.bindings !tag_map)
+
 let parse_color_config str =
   let styles = Terminal.parse str in
   init_tag_map styles
@@ -264,13 +276,13 @@ let make_printing_functions () =
     let (tpfx, ttag) = split_tag tag in
     if tpfx <> end_pfx then
       let style = get_style ttag in
-      match style.Terminal.prefix with Some s -> Format.pp_print_string ft s | None -> () in
+      match style.Terminal.prefix with Some s -> Format.pp_print_as ft 0 s | None -> () in
 
   let print_suffix ft tag =
     let (tpfx, ttag) = split_tag tag in
     if tpfx <> start_pfx then
       let style = get_style ttag in
-      match style.Terminal.suffix with Some s -> Format.pp_print_string ft s | None -> () in
+      match style.Terminal.suffix with Some s -> Format.pp_print_as ft 0 s | None -> () in
 
   print_prefix, print_suffix
 
diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli
index b0e3b3772c..a1e289cd5a 100644
--- a/vernac/topfmt.mli
+++ b/vernac/topfmt.mli
@@ -46,6 +46,7 @@ val emacs_logger : ?pre_hdr:Pp.t -> Feedback.level -> Pp.t -> unit
 val default_styles : unit -> unit
 val parse_color_config : string -> unit
 val dump_tags : unit -> (string * Terminal.style) list
+val set_emacs_print_strings : unit -> unit
 
 (** Initialization of interpretation of tags *)
 val init_terminal_output : color:bool -> unit