Adding support for bindings tags to explicit prefix/suffix rather than colors.

This is usable for no-color terminal.

For instance, a typical application in mind is the Coq-generate names
marker which can be rendered with a color if the interface supports it
and a prefix "~" if the interface does not support colors.

5 files changed, 64 insertions, 16 deletions

diff --git a/lib/terminal.ml b/lib/terminal.ml
index 3b6e34f0b..34efddfbc 100644
--- a/lib/terminal.ml
+++ b/lib/terminal.ml
@@ -35,6 +35,8 @@ type style = {
   italic : bool option;
   underline : bool option;
   negative : bool option;
+  prefix : string option;
+  suffix : string option;
 }
 
 let set o1 o2 = match o1 with
@@ -51,9 +53,11 @@ let default = {
   italic = None;
   underline = None;
   negative = None;
+  prefix = None;
+  suffix = None;
 }
 
-let make ?fg_color ?bg_color ?bold ?italic ?underline ?negative ?style () =
+let make ?fg_color ?bg_color ?bold ?italic ?underline ?negative ?style ?prefix ?suffix () =
   let st = match style with
   | None -> default
   | Some st -> st
@@ -65,6 +69,8 @@ let make ?fg_color ?bg_color ?bold ?italic ?underline ?negative ?style () =
     italic = set st.italic italic;
     underline = set st.underline underline;
     negative = set st.negative negative;
+    prefix = set st.prefix prefix;
+    suffix = set st.suffix suffix;
   }
 
 let merge s1 s2 =
@@ -75,6 +81,8 @@ let merge s1 s2 =
     italic = set s1.italic s2.italic;
     underline = set s1.underline s2.underline;
     negative = set s1.negative s2.negative;
+    prefix = set s1.prefix s2.prefix;
+    suffix = set s1.suffix s2.suffix;
   }
 
 let base_color = function
@@ -168,6 +176,8 @@ let reset_style = {
   italic = Some false;
   underline = Some false;
   negative = Some false;
+  prefix = None;
+  suffix = None;
 }
 
 let has_style t =
diff --git a/lib/terminal.mli b/lib/terminal.mli
index dbc418dd6..b1b76e6e2 100644
--- a/lib/terminal.mli
+++ b/lib/terminal.mli
@@ -35,11 +35,14 @@ type style = {
   italic : bool option;
   underline : bool option;
   negative : bool option;
+  prefix : string option;
+  suffix : string option;
 }
 
 val make : ?fg_color:color -> ?bg_color:color ->
   ?bold:bool -> ?italic:bool -> ?underline:bool ->
-  ?negative:bool -> ?style:style -> unit -> style
+  ?negative:bool -> ?style:style ->
+  ?prefix:string -> ?suffix:string -> unit -> style
 (** Create a style from the given flags. It is derived from the optional
     [style] argument if given. *)
 
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 8c394316e..08c235023 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -58,16 +58,18 @@ let init_color () =
     match colors with
     | None ->
       (** Default colors *)
-      Topfmt.init_color_output ()
+      Topfmt.init_terminal_output ~color:true
     | Some "" ->
       (** No color output *)
-      ()
+      Topfmt.init_terminal_output ~color:false
     | Some s ->
       (** Overwrite all colors *)
       Topfmt.clear_styles ();
       Topfmt.parse_color_config s;
-      Topfmt.init_color_output ()
+      Topfmt.init_terminal_output ~color:true
   end
+  else
+    Topfmt.init_terminal_output ~color:false
 
 let toploop_init = ref begin fun x ->
   let () = init_color () in
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index b3810f7d5..e7b14309d 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -149,7 +149,7 @@ let gen_logger dbg warn ?pre_hdr level msg = match level with
 (** Standard loggers *)
 
 (* We provide a generic clear_log_backend callback for backends
-   wanting to do clenaup after the print.
+   wanting to do cleanup after the print.
 *)
 let std_logger_cleanup = ref (fun () -> ())
 
@@ -207,6 +207,8 @@ let make_style_stack () =
       italic = Some false;
       underline = Some false;
       negative = Some false;
+      prefix = None;
+      suffix = None;
     })
   in
   let style_stack = ref [] in
@@ -235,20 +237,49 @@ let make_style_stack () =
   let clear () = style_stack := [] in
   push, pop, clear
 
-let init_color_output () =
+let make_printing_functions () =
+  let empty = Terminal.make () in
+  let print_prefix ft tag =
+    let style =
+      try CString.Map.find tag !tag_map
+      with | Not_found -> empty
+    in
+    match style.Terminal.prefix with Some s -> Format.pp_print_string ft s | None -> ()
+  in
+  let print_suffix ft tag =
+    let style =
+      try CString.Map.find tag !tag_map
+      with | Not_found -> empty
+    in
+    match style.Terminal.suffix with Some s -> Format.pp_print_string ft s | None -> ()
+  in
+  print_prefix, print_suffix
+
+let init_terminal_output ~color =
   init_tag_map (default_tag_map ());
   let push_tag, pop_tag, clear_tag = make_style_stack () in
-  std_logger_cleanup := clear_tag;
-  let tag_handler = {
+  let print_prefix, print_suffix = make_printing_functions () in
+  let tag_handler ft = {
     Format.mark_open_tag   = push_tag;
     Format.mark_close_tag  = pop_tag;
-    Format.print_open_tag  = ignore;
-    Format.print_close_tag = ignore;
+    Format.print_open_tag  = print_prefix ft;
+    Format.print_close_tag = print_suffix ft;
   } in
-  Format.pp_set_mark_tags !std_ft true;
-  Format.pp_set_mark_tags !err_ft true;
-  Format.pp_set_formatter_tag_functions !std_ft tag_handler;
-  Format.pp_set_formatter_tag_functions !err_ft tag_handler
+  if color then
+    (* Use 0-length markers *)
+    begin
+      std_logger_cleanup := clear_tag;
+      Format.pp_set_mark_tags !std_ft true;
+      Format.pp_set_mark_tags !err_ft true
+    end
+  else
+    (* Use textual markers *)
+    begin
+      Format.pp_set_print_tags !std_ft true;
+      Format.pp_set_print_tags !err_ft true
+    end;
+  Format.pp_set_formatter_tag_functions !std_ft (tag_handler !std_ft);
+  Format.pp_set_formatter_tag_functions !err_ft (tag_handler !err_ft)
 
 (* Rules for emacs:
    - Debug/info: emacs_quote_info
diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli
index 0e781bcc1..6e006fc6c 100644
--- a/vernac/topfmt.mli
+++ b/vernac/topfmt.mli
@@ -41,11 +41,13 @@ val std_logger   : ?pre_hdr:Pp.std_ppcmds -> Feedback.level -> Pp.std_ppcmds ->
 val emacs_logger : ?pre_hdr:Pp.std_ppcmds -> Feedback.level -> Pp.std_ppcmds -> unit
 
 (** Color output *)
-val init_color_output : unit -> unit
 val clear_styles : unit -> unit
 val parse_color_config : string -> unit
 val dump_tags : unit -> (string * Terminal.style) list
 
+(** Initialization of interpretation of tags *)
+val init_terminal_output : color:bool -> unit
+
 (** Error printing *)
 (* To be deprecated when we can fully move to feedback-based error
    printing. *)