From 496d9d4007f59e6114dae9a94ee5a39d241484cf Mon Sep 17 00:00:00 2001 From: Jim Date: Tue, 27 Mar 2018 12:23:08 -0700 Subject: 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). --- clib/terminal.ml | 48 ++++++++++++++++++++++++++++++++++-------------- clib/terminal.mli | 6 ++++++ 2 files changed, 40 insertions(+), 14 deletions(-) (limited to 'clib') 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. *) -- cgit v1.2.3 From 8de046df97b1ea391a3f3879c20c74d53c9fba48 Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Mon, 9 Apr 2018 13:16:46 -0700 Subject: Displays the differences between successive proof steps in coqtop and CoqIDE. Proof General requires minor changes to make the diffs visible, but this code shouldn't break the existing version of PG. Diffs are computed for the hypotheses and conclusion of the first goal between the old and new proofs. Strings are split into tokens using the Coq lexer, then the list of tokens are diffed using the Myers algorithm. A fixup routine (Pp_diff.shorten_diff_span) shortens the span of the diff result in some cases. Diffs can be enabled with the Coq commmand "Set Diffs on|off|removed." or "-diffs on|off|removed" on the OS command line. The "on" option shows only the new item with added text, while "removed" shows each modified item twice--once with the old value showing removed text and once with the new value showing added text. The highlights use 4 tags to specify the color and underline/strikeout. These are "diffs.added", "diffs.removed", "diffs.added.bg" and "diffs.removed.bg". The first two are for added or removed text; the last two are for unmodified parts of a modified item. Diffs that span multiple strings in the Pp are tagged with "start.diff.*" and "end.diff.*", but only on the first and last strings of the span. --- clib/clib.mllib | 2 + clib/diff2.ml | 158 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ clib/diff2.mli | 101 ++++++++++++++++++++++++++++++++++++ 3 files changed, 261 insertions(+) create mode 100644 clib/diff2.ml create mode 100644 clib/diff2.mli (limited to 'clib') diff --git a/clib/clib.mllib b/clib/clib.mllib index afece4074c..5a2c9a9ce9 100644 --- a/clib/clib.mllib +++ b/clib/clib.mllib @@ -37,3 +37,5 @@ Backtrace IStream Terminal Monad + +Diff2 diff --git a/clib/diff2.ml b/clib/diff2.ml new file mode 100644 index 0000000000..42c4733fed --- /dev/null +++ b/clib/diff2.ml @@ -0,0 +1,158 @@ +(* copied from https://github.com/leque/ocaml-diff.git and renamed from "diff.ml" *) + +(* + * Copyright (C) 2016 OOHASHI Daichi + * + * Permission is hereby granted, free of charge, to any person obtaining a copy + * of this software and associated documentation files (the "Software"), to deal + * in the Software without restriction, including without limitation the rights + * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell + * copies of the Software, and to permit persons to whom the Software is + * furnished to do so, subject to the following conditions: + * The above copyright notice and this permission notice shall be included in + * all copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN + * THE SOFTWARE. + *) + +type 'a common = + [ `Common of int * int * 'a ] + +type 'a edit = + [ `Added of int * 'a + | `Removed of int * 'a + | 'a common + ] + +module type SeqType = sig + type t + type elem + val get : t -> int -> elem + val length : t -> int +end + +module type S = sig + type t + type elem + + val lcs : + ?equal:(elem -> elem -> bool) -> + t -> t -> elem common list + + val diff : + ?equal:(elem -> elem -> bool) -> + t -> t -> elem edit list + + val fold_left : + ?equal:(elem -> elem -> bool) -> + f:('a -> elem edit -> 'a) -> + init:'a -> + t -> t -> 'a + + val iter : + ?equal:(elem -> elem -> bool) -> + f:(elem edit -> unit) -> + t -> t -> unit +end + +module Make(M : SeqType) : (S with type t = M.t and type elem = M.elem) = struct + type t = M.t + type elem = M.elem + + let lcs ?(equal = (=)) a b = + let n = M.length a in + let m = M.length b in + let mn = m + n in + let sz = 2 * mn + 1 in + let vd = Array.make sz 0 in + let vl = Array.make sz 0 in + let vr = Array.make sz [] in + let get v i = Array.get v (i + mn) in + let set v i x = Array.set v (i + mn) x in + let finish () = + let rec loop i maxl r = + if i > mn then + List.rev r + else if get vl i > maxl then + loop (i + 1) (get vl i) (get vr i) + else + loop (i + 1) maxl r + in loop (- mn) 0 [] + in + if mn = 0 then + [] + else + (* For d <- 0 to mn Do *) + let rec dloop d = + assert (d <= mn); + (* For k <- -d to d in steps of 2 Do *) + let rec kloop k = + if k > d then + dloop @@ d + 1 + else + let x, l, r = + if k = -d || (k <> d && get vd (k - 1) < get vd (k + 1)) then + get vd (k + 1), get vl (k + 1), get vr (k + 1) + else + get vd (k - 1) + 1, get vl (k - 1), get vr (k - 1) + in + let x, y, l, r = + let rec xyloop x y l r = + if x < n && y < m && equal (M.get a x) (M.get b y) then + xyloop (x + 1) (y + 1) (l + 1) (`Common(x, y, M.get a x) :: r) + else + x, y, l, r + in xyloop x (x - k) l r + in + set vd k x; + set vl k l; + set vr k r; + if x >= n && y >= m then + (* Stop *) + finish () + else + kloop @@ k + 2 + in kloop @@ -d + in dloop 0 + + let fold_left ?(equal = (=)) ~f ~init a b = + let ff x y = f y x in + let fold_map f g x from to_ init = + let rec loop i init = + if i >= to_ then + init + else + loop (i + 1) (f (g i @@ M.get x i) init) + in loop from init + in + let added i x = `Added (i, x) in + let removed i x = `Removed (i, x) in + let rec loop cs apos bpos init = + match cs with + | [] -> + init + |> fold_map ff removed a apos (M.length a) + |> fold_map ff added b bpos (M.length b) + | `Common (aoff, boff, _) as e :: rest -> + init + |> fold_map ff removed a apos aoff + |> fold_map ff added b bpos boff + |> ff e + |> loop rest (aoff + 1) (boff + 1) + in loop (lcs ~equal a b) 0 0 init + + let diff ?(equal = (=)) a b = + fold_left ~equal ~f:(fun xs x -> x::xs) ~init:[] a b + + let iter ?(equal = (=)) ~f a b = + fold_left a b + ~equal + ~f:(fun () x -> f x) + ~init:() +end diff --git a/clib/diff2.mli b/clib/diff2.mli new file mode 100644 index 0000000000..a085f4ffe8 --- /dev/null +++ b/clib/diff2.mli @@ -0,0 +1,101 @@ +(* copied from https://github.com/leque/ocaml-diff.git and renamed from "diff.mli" *) +(** + An implementation of Eugene Myers' O(ND) Difference Algorithm\[1\]. + This implementation is a port of util.lcs module of + {{:http://practical-scheme.net/gauche} Gauche Scheme interpreter}. + + - \[1\] Eugene Myers, An O(ND) Difference Algorithm and Its Variations, Algorithmica Vol. 1 No. 2, pp. 251-266, 1986. + *) + +type 'a common = [ + `Common of int * int * 'a + ] +(** an element of lcs of seq1 and seq2 *) + +type 'a edit = + [ `Removed of int * 'a + | `Added of int * 'a + | 'a common + ] +(** an element of diff of seq1 and seq2. *) + +module type SeqType = sig + type t + (** The type of the sequence. *) + + type elem + (** The type of the elements of the sequence. *) + + val get : t -> int -> elem + (** [get t n] returns [n]-th element of the sequence [t]. *) + + val length : t -> int + (** [length t] returns the length of the sequence [t]. *) +end +(** Input signature of {!Diff.Make}. *) + +module type S = sig + type t + (** The type of input sequence. *) + + type elem + (** The type of the elements of result / input sequence. *) + + val lcs : + ?equal:(elem -> elem -> bool) -> + t -> t -> elem common list + (** + [lcs ~equal seq1 seq2] computes the LCS (longest common sequence) of + [seq1] and [seq2]. + Elements of [seq1] and [seq2] are compared with [equal]. + [equal] defaults to [Pervasives.(=)]. + + Elements of lcs are [`Common (pos1, pos2, e)] + where [e] is an element, [pos1] is a position in [seq1], + and [pos2] is a position in [seq2]. + *) + + val diff : + ?equal:(elem -> elem -> bool) -> + t -> t -> elem edit list + (** + [diff ~equal seq1 seq2] computes the diff of [seq1] and [seq2]. + Elements of [seq1] and [seq2] are compared with [equal]. + + Elements only in [seq1] are represented as [`Removed (pos, e)] + where [e] is an element, and [pos] is a position in [seq1]; + those only in [seq2] are represented as [`Added (pos, e)] + where [e] is an element, and [pos] is a position in [seq2]; + those common in [seq1] and [seq2] are represented as + [`Common (pos1, pos2, e)] + where [e] is an element, [pos1] is a position in [seq1], + and [pos2] is a position in [seq2]. + *) + + val fold_left : + ?equal:(elem -> elem -> bool) -> + f:('a -> elem edit -> 'a) -> + init:'a -> + t -> t -> 'a + (** + [fold_left ~equal ~f ~init seq1 seq2] is same as + [diff ~equal seq1 seq2 |> ListLabels.fold_left ~f ~init], + but does not create an intermediate list. + *) + + val iter : + ?equal:(elem -> elem -> bool) -> + f:(elem edit -> unit) -> + t -> t -> unit + (** + [iter ~equal ~f seq1 seq2] is same as + [diff ~equal seq1 seq2 |> ListLabels.iter ~f], + but does not create an intermediate list. + *) +end +(** Output signature of {!Diff.Make}. *) + +module Make : + functor (M : SeqType) -> (S with type t = M.t and type elem = M.elem) +(** Functor building an implementation of the diff structure + given a sequence type. *) -- cgit v1.2.3