Pp_diffComputes the differences between 2 Pp's and adds additional tags to a Pp to highlight them. Strings are split into tokens using the Coq lexer, then the lists of tokens are diffed using the Myers algorithm. A fixup routine, shorten_diff_span, shortens the span of the diff result in some cases.
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.
If the inputs are not acceptable to the lexer, break the strings into lists of tokens and call diff_strs, then add_diff_tags with a Pp.t that matches the input lists of strings. Tokens that the lexer doesn't return exactly as they appeared in the input will raise an exception in add_diff_tags (e.g. comments and quoted strings). Fixing that requires tweaking the lexer.
Limitations/Possible enhancements:
Compute the diff between two Pp.t structures and return versions of each with diffs highlighted as (old, new)
val diff_pp_combined : ?tokenize_string:(string -> string list) ->
?show_removed:bool -> Pp.t -> Pp.t -> Pp.tCompute the diff between two Pp.t structures and return a highlighted Pp.t. If show_removed is true, show separate lines for removals and additions, otherwise only show additions
module StringDiff : sig ... endtype diff_list = StringDiff.elem Diff2.edit listval diff_str : ?tokenize_string:(string -> string list) -> string -> string -> StringDiff.elem Diff2.edit listCompute the difference between 2 strings in terms of tokens, using the lexer to identify tokens.
If the strings are not lexable, this routine will raise Diff_Failure. (I expect to modify the lexer soon so this won't happen.)
Therefore you should catch any exceptions. The workaround for now is for the caller to tokenize the strings itself and then call diff_strs.
val diff_strs : StringDiff.t -> StringDiff.t -> StringDiff.elem Diff2.edit listCompute the differences between 2 lists of strings, treating the strings in the lists as indivisible units.
val add_diff_tags : diff_type -> Pp.t -> StringDiff.elem Diff2.edit list -> Pp.tGenerate a new Pp that adds tags marking diffs to a Pp structure: which: either `Added or `Removed, indicates which type of diffs to add pp: the original structure. For `Added, must be the new pp passed to diff_pp For `Removed, must be the old pp passed to diff_pp. Passing the wrong one will likely raise Diff_Failure. diffs: the diff list returned by diff_pp
Diffs of single strings in the Pp are tagged with "diff.added" or "diff.removed". Diffs that span multiple strings in the Pp are tagged with "start.diff.*" or "end.diff.*", but only on the first and last strings of the span.
Ppcmd_strings will be split into multiple Ppcmd_strings if a diff starts or ends in the middle of the string. Whitespace just before or just after a diff will not be part of the highlight.
Preexisting tags in pp may contain only a single Ppcmd_string. Those tags will be placed inside the diff tags to ensure proper nesting of tags within spans of "start.diff.*" ... "end.diff.*".
Under some "impossible" conditions, this routine may raise Diff_Failure. If you want to make your call especially bulletproof, catch this exception, print a user-visible message, then recall this routine with the first argument set to None, which will skip the diff.
val has_changes : diff_list -> bool * boolReturns a boolean pair (added, removed) for diffs where a true value indicates that something was added/removed in the diffs.
val get_dinfo : StringDiff.elem Diff2.edit -> diff_type * stringReturns a modified pp with the background highlighted with "start.<diff_tag>.bg" and "end.<diff_tag>.bg" tags at the beginning and end of the returned Pp.t
val string_of_diffs : diff_list -> stringDisplays the diffs to a printable format for debugging