diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-07-05 22:52:09 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-07-08 11:31:52 +0200 |
commit | dbf1f8200c6d5d3ddb61aa093376cb78156980e1 (patch) | |
tree | f794b67e8498bba9b2b7633e9181a566cba874e2 | |
parent | 38a749767b74c1fc67d02948efd13ea8c5cbcd0b (diff) |
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.
-rw-r--r-- | lib/terminal.ml | 12 | ||||
-rw-r--r-- | lib/terminal.mli | 5 | ||||
-rw-r--r-- | toplevel/coqtop.ml | 8 | ||||
-rw-r--r-- | vernac/topfmt.ml | 51 | ||||
-rw-r--r-- | vernac/topfmt.mli | 4 |
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. *) |