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.

1 files changed, 64 insertions, 0 deletions

diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli
new file mode 100644
index 0000000000..481b664d8a
--- /dev/null
+++ b/printing/proof_diffs.mli
@@ -0,0 +1,64 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* diff options *)
+
+(** Controls whether to show diffs.  Takes values "on", "off", "removed" *)
+val write_diffs_option : string -> unit
+(** Returns true if the diffs option is "on" or "removed" *)
+val show_diffs : unit -> bool
+
+(** Computes the diff between the first goal of two Proofs and returns
+the highlighted hypotheses and conclusion.
+
+If the strings used to display the goal are not lexable (this is believed
+unlikely), this routine will generate a Diff_Failure.  This routine may also
+raise Diff_Failure under some "impossible" conditions.
+
+If you want to make your call especially bulletproof, catch these
+exceptions, print a user-visible message, then recall this routine with
+the first argument set to None, which will skip the diff.
+*)
+val diff_first_goal : Proof.t option -> Proof.t option -> Pp.t list * Pp.t
+
+open Evd
+open Proof_type
+
+(** Computes the diff between two goals
+
+If the strings used to display the goal are not lexable (this is believed
+unlikely), this routine will generate a Diff_Failure.  This routine may also
+raise Diff_Failure under some "impossible" conditions.
+
+If you want to make your call especially bulletproof, catch these
+exceptions, print a user-visible message, then recall this routine with
+the first argument set to None, which will skip the diff.
+*)
+val diff_goals : ?prev_gs:(goal sigma) -> goal sigma option -> Pp.t
+
+(* Exposed for unit test, don't use these otherwise *)
+(* output channel for the test log file *)
+val log_out_ch : out_channel ref
+
+
+type hyp_info = {
+  idents: string list;
+  rhs_pp: Pp.t;
+  mutable done_: bool;
+}
+
+module StringMap :
+sig
+  type +'a t
+  val empty: hyp_info t
+  val add : string -> hyp_info -> hyp_info t -> hyp_info t
+end
+
+val diff_hyps : string list list -> hyp_info StringMap.t -> string list list -> hyp_info StringMap.t -> Pp.t list