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/diff2.mli | 101 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 101 insertions(+)
 create mode 100644 clib/diff2.mli

(limited to 'clib/diff2.mli')

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