Generate more compact escape sequences by

a) not explicitly setting the default value and
b) not repeating attributes that are already set.

Example (omitting escape character):
Old:  E : [92;49;22;23;24;27mev[39;49;22;23;24;27m [39;49;22;23;24;27mn[39;49;22;23;24;27m
New:  E : [92mev[0m n

(92 is bright green, the other codes set default attributes).

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