diff options
| -rw-r--r-- | clib/terminal.ml | 48 | ||||
| -rw-r--r-- | clib/terminal.mli | 6 | ||||
| -rw-r--r-- | vernac/topfmt.ml | 28 |
3 files changed, 51 insertions, 31 deletions
diff --git a/clib/terminal.ml b/clib/terminal.ml index 1d9468137b..d243d6599e 100644 --- a/clib/terminal.ml +++ b/clib/terminal.ml @@ -59,6 +59,19 @@ let default = { suffix = None; } +let reset = "\027[0m" + +let reset_style = { + fg_color = Some `DEFAULT; + bg_color = Some `DEFAULT; + bold = Some false; + italic = Some false; + underline = Some false; + negative = Some false; + prefix = None; + suffix = None; +} + let make ?fg_color ?bg_color ?bold ?italic ?underline ?negative ?style ?prefix ?suffix () = let st = match style with | None -> default @@ -87,6 +100,25 @@ let merge s1 s2 = suffix = set s1.suffix s2.suffix; } +let diff s1 s2 = + let diff_op o1 o2 reset_val = match o1 with + | None -> o2 + | Some _ -> + match o2 with + | None -> reset_val + | Some _ -> if o1 = o2 then None else o2 in + + { + fg_color = diff_op s1.fg_color s2.fg_color reset_style.fg_color; + bg_color = diff_op s1.bg_color s2.bg_color reset_style.bg_color; + bold = diff_op s1.bold s2.bold reset_style.bold; + italic = diff_op s1.italic s2.italic reset_style.italic; + underline = diff_op s1.underline s2.underline reset_style.underline; + negative = diff_op s1.negative s2.negative reset_style.negative; + prefix = diff_op s1.prefix s2.prefix reset_style.prefix; + suffix = diff_op s1.suffix s2.suffix reset_style.suffix; + } + let base_color = function | `DEFAULT -> 9 | `BLACK -> 0 @@ -167,20 +199,8 @@ let repr st = let eval st = let tags = repr st in let tags = List.map string_of_int tags in - Printf.sprintf "\027[%sm" (String.concat ";" tags) - -let reset = "\027[0m" - -let reset_style = { - fg_color = Some `DEFAULT; - bg_color = Some `DEFAULT; - bold = Some false; - italic = Some false; - underline = Some false; - negative = Some false; - prefix = None; - suffix = None; -} + if List.length tags = 0 then "" else + Printf.sprintf "\027[%sm" (String.concat ";" tags) let has_style t = Unix.isatty t && Sys.os_type = "Unix" diff --git a/clib/terminal.mli b/clib/terminal.mli index dbf8d4640c..bc30b0016f 100644 --- a/clib/terminal.mli +++ b/clib/terminal.mli @@ -51,6 +51,9 @@ val make : ?fg_color:color -> ?bg_color:color -> val merge : style -> style -> style (** [merge s1 s2] returns [s1] with all defined values of [s2] overwritten. *) +val diff : style -> style -> style +(** [diff s1 s2] returns the differences between [s1] and [s2]. *) + val repr : style -> int list (** Generate the ANSI code representing the given style. *) @@ -60,6 +63,9 @@ val eval : style -> string val reset : string (** This escape sequence resets all attributes. *) +val reset_style : style +(** The default style *) + val has_style : Unix.file_descr -> bool (** Whether an output file descriptor handles styles. Very heuristic, only checks it is a terminal. *) diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index 609dac69aa..ecf9733041 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -203,17 +203,7 @@ let dump_tags () = CString.Map.bindings !tag_map let make_style_stack () = (** Default tag is to reset everything *) let empty = Terminal.make () in - let default_tag = Terminal.({ - fg_color = Some `DEFAULT; - bg_color = Some `DEFAULT; - bold = Some false; - italic = Some false; - underline = Some false; - negative = Some false; - prefix = None; - suffix = None; - }) - in + let default_tag = Terminal.reset_style in let style_stack = ref [] in let peek () = match !style_stack with | [] -> default_tag (** Anomalous case, but for robustness *) @@ -224,18 +214,22 @@ let make_style_stack () = try CString.Map.find tag !tag_map with | Not_found -> empty in - (** Use the merging of the latest tag and the one being currently pushed. - This may be useful if for instance the latest tag changes the background and - the current one the foreground, so that the two effects are additioned. *) + (** Merge the current settings and the style being pushed. This allows + restoring the previous settings correctly in a pop when both set the same + attribute. Example: current settings have red FG, the pushed style has + green FG. When popping the style, we should set red FG, not default FG. *) let style = Terminal.merge (peek ()) style in + let diff = Terminal.diff (peek ()) style in style_stack := style :: !style_stack; - Terminal.eval style + Terminal.eval diff in let pop _ = match !style_stack with | [] -> (** Something went wrong, we fallback *) Terminal.eval default_tag - | _ :: rem -> style_stack := rem; - Terminal.eval (peek ()) + | cur :: rem -> style_stack := rem; + if cur = (peek ()) then "" else + if List.length rem = 0 then Terminal.reset else + Terminal.eval (Terminal.diff cur (peek ())) in let clear () = style_stack := [] in push, pop, clear |