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, 12 insertions, 6 deletions

diff --git a/printing/printer.mli b/printing/printer.mli
index eddfef6fad..948b06f3f6 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -171,22 +171,26 @@ val pr_transparent_state   : transparent_state -> Pp.t
 
 (** Proofs, these functions obey [Hyps Limit] and [Compact contexts]. *)
 
-val pr_goal                : goal sigma -> Pp.t
+val pr_goal                : ?diffs:bool -> ?prev_gs:(goal sigma) -> goal sigma -> Pp.t
 
-(** [pr_subgoals ~pr_first pp sigma seeds shelf focus_stack unfocused goals]
+(** [pr_subgoals ~pr_first ~prev_proof pp sigma seeds shelf focus_stack unfocused goals]
    prints the goals of the list [goals] followed by the goals in
    [unfocused], in a short way (typically only the conclusion) except
-   for the first goal if [pr_first] is true. This function can be
-   replaced by another one by calling [set_printer_pr] (see below),
-   typically by plugin writers. The default printer prints only the
+   for the first goal if [pr_first] is true. Also, if [diffs] is true
+   and [pr_first] is true, then highlight diffs relative to [prev] in the
+   output for first goal. This function prints only the
    focused goals unless the conrresponding option
    [enable_unfocused_goal_printing] is set. [seeds] is for printing
    dependent evars (mainly for emacs proof tree mode). *)
-val pr_subgoals            : ?pr_first:bool -> Pp.t option -> evar_map -> seeds:goal list -> shelf:goal list -> stack:int list -> unfocused:goal list -> goals:goal list -> Pp.t
+val pr_subgoals            : ?pr_first:bool -> ?diffs:bool -> ?prev:(goal list * evar_map) -> Pp.t option -> evar_map
+                             -> seeds:goal list -> shelf:goal list -> stack:int list
+                             -> unfocused: goal list -> goals:goal list -> Pp.t
 
 val pr_subgoal             : int -> evar_map -> goal list -> Pp.t
 val pr_concl               : int -> evar_map -> goal -> Pp.t
 
+val pr_open_subgoals_diff  : ?quiet:bool -> ?diffs:bool -> ?prev_proof:Proof.t -> Proof.t -> Pp.t
+val diff_pr_open_subgoals  : ?quiet:bool -> Proof.t option -> Proof.t option -> Pp.t
 val pr_open_subgoals       : proof:Proof.t -> Pp.t
 val pr_nth_open_subgoal    : proof:Proof.t -> int -> Pp.t
 val pr_evar                : evar_map -> (Evar.t * evar_info) -> Pp.t
@@ -197,6 +201,8 @@ val pr_ne_evar_set         : Pp.t -> Pp.t -> evar_map ->
 
 val pr_prim_rule           : prim_rule -> Pp.t
 
+val print_and_diff : Proof.t option -> Proof.t option -> unit
+
 (** Backwards compatibility *)
 
 val prterm                 : constr -> Pp.t (** = pr_lconstr *)