Merge PR #10019: Update behavior of -emacs to support showing diffs in ProofGeneral (master branch)

Reviewed-by: ejgallego

5 files changed, 26 insertions, 9 deletions

diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 319f5c8ad6..9a18baa0bc 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -34,7 +34,7 @@ let set_type_in_type () =
 
 (******************************************************************************)
 
-type color = [`ON | `AUTO | `OFF]
+type color = [`ON | `AUTO | `EMACS | `OFF]
 
 type native_compiler = NativeOff | NativeOn of { ondemand : bool }
 
@@ -171,7 +171,7 @@ let add_load_vernacular opts verb s =
 (** Options for proof general *)
 let set_emacs opts =
   Printer.enable_goal_tags_printing := true;
-  { opts with color = `OFF; print_emacs = true }
+  { opts with color = `EMACS; print_emacs = true }
 
 let set_color opts = function
 | "yes" | "on" -> { opts with color = `ON }
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index 9bcfdca332..d7f9819bee 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-type color = [`ON | `AUTO | `OFF]
+type color = [`ON | `AUTO | `EMACS | `OFF]
 
 val default_toplevel : Names.DirPath.t
 
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 15172b30f8..9323a57417 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -113,6 +113,7 @@ let fatal_error_exn exn =
 let init_color opts =
   let has_color = match opts.color with
   | `OFF -> false
+  | `EMACS -> false
   | `ON -> true
   | `AUTO ->
     Terminal.has_style Unix.stdout &&
@@ -133,10 +134,13 @@ let init_color opts =
       Topfmt.default_styles (); false                 (* textual markers, no color *)
     end
   in
-  if not term_color then
-    Proof_diffs.write_color_enabled term_color;
-  if Proof_diffs.show_diffs () && not term_color then
-    (prerr_endline "Error: -diffs requires enabling -color"; exit 1);
+  if opts.color = `EMACS then
+    Topfmt.set_emacs_print_strings ()
+  else if not term_color then begin
+      Proof_diffs.write_color_enabled term_color;
+    if Proof_diffs.show_diffs () then
+      (prerr_endline "Error: -diffs requires enabling -color"; exit 1)
+  end;
   Topfmt.init_terminal_output ~color:term_color
 
 let print_style_tags opts =
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