From 5ec7eca640a6ee495eb2c0fb8d8a4076256ff96d Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Sat, 6 Jul 2019 19:25:39 -0700 Subject: Show diffs in "Show Proof." Add experimental "Show Proof" command to the toplevel that shadows the current command in the parser (in coqtop and PG only). Apply existing code to highlight diffs in the output --- .../07-commands-and-options/10494-diffs-in-show-proof.rst | 6 ++++++ doc/sphinx/proof-engine/proof-handling.rst | 15 ++++++++++++--- 2 files changed, 18 insertions(+), 3 deletions(-) create mode 100644 doc/changelog/07-commands-and-options/10494-diffs-in-show-proof.rst (limited to 'doc') diff --git a/doc/changelog/07-commands-and-options/10494-diffs-in-show-proof.rst b/doc/changelog/07-commands-and-options/10494-diffs-in-show-proof.rst new file mode 100644 index 0000000000..c1df728c5c --- /dev/null +++ b/doc/changelog/07-commands-and-options/10494-diffs-in-show-proof.rst @@ -0,0 +1,6 @@ +- Optionally highlight the differences between successive proof steps in the + :cmd:`Show Proof` command. Experimental; only available in coqtop + and Proof General for now, may be supported in other IDEs + in the future. + (`#10494 `_, + by Jim Fehrle). diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 57a54bc0ad..00f8269dc3 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -535,7 +535,7 @@ Requesting information eexists ?[n]. Show n. - .. cmdv:: Show Proof + .. cmdv:: Show Proof {? Diffs {? removed } } :name: Show Proof Displays the proof term generated by the tactics @@ -544,6 +544,12 @@ Requesting information constructed. Each hole is an existential variable, which appears as a question mark followed by an identifier. + Experimental: Specifying “Diffs” highlights the difference between the + current and previous proof step. By default, the command shows the + output once with additions highlighted. Including “removed” shows + the output twice: once showing removals and once showing additions. + It does not examine the :opt:`Diffs` option. See :ref:`showing_diffs`. + .. cmdv:: Show Conjectures :name: Show Conjectures @@ -624,8 +630,11 @@ Showing differences between proof steps --------------------------------------- -Coq can automatically highlight the differences between successive proof steps and between -values in some error messages. +Coq can automatically highlight the differences between successive proof steps +and between values in some error messages. Also, as an experimental feature, +Coq can also highlight differences between proof steps shown in the :cmd:`Show Proof` +command, but only, for now, when using coqtop and Proof General. + For example, the following screenshots of CoqIDE and coqtop show the application of the same :tacn:`intros` tactic. The tactic creates two new hypotheses, highlighted in green. The conclusion is entirely in pale green because although it’s changed, no tokens were added -- cgit v1.2.3