diff options
| author | Jim Fehrle | 2018-04-09 13:16:46 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2018-07-23 20:13:19 -0700 |
| commit | 8de046df97b1ea391a3f3879c20c74d53c9fba48 (patch) | |
| tree | 3d1d3aed23093b3c2874a9a480d78400432f15cb /toplevel/coqloop.ml | |
| parent | a6131723faa8699e485a88fae8cc2323b82a8461 (diff) | |
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.
Diffstat (limited to 'toplevel/coqloop.ml')
| -rw-r--r-- | toplevel/coqloop.ml | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 7ae15ac100..7b7e1b16c0 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -318,12 +318,6 @@ let loop_flush_all () = Format.pp_print_flush !Topfmt.std_ft (); Format.pp_print_flush !Topfmt.err_ft () -let pr_open_cur_subgoals () = - try - let proof = Proof_global.give_me_the_proof () in - Printer.pr_open_subgoals ~proof - with Proof_global.NoCurrentProof -> Pp.str "" - (* Goal equality heuristic. *) let pequal cmp1 cmp2 (a1,a2) (b1,b2) = cmp1 a1 b1 && cmp2 a2 b2 let evleq e1 e2 = CList.equal Evar.equal e1 e2 @@ -346,7 +340,7 @@ let top_goal_print oldp newp = let proof_changed = not (Option.equal cproof oldp newp) in let print_goals = not !Flags.quiet && proof_changed && Proof_global.there_are_pending_proofs () in - if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ()) + if print_goals then Printer.print_and_diff oldp newp; with | exn -> let (e, info) = CErrors.push exn in |