diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/_static/diffs-error-message.png | bin | 0 -> 5607 bytes | |||
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 16 |
2 files changed, 13 insertions, 3 deletions
diff --git a/doc/sphinx/_static/diffs-error-message.png b/doc/sphinx/_static/diffs-error-message.png Binary files differnew file mode 100644 index 0000000000..6733d9c6a9 --- /dev/null +++ b/doc/sphinx/_static/diffs-error-message.png diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 27360f02d3..07215a0c7e 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -628,7 +628,8 @@ Showing differences between proof steps --------------------------------------- -Coq can automatically highlight the differences between successive proof steps. +Coq can automatically highlight the differences between successive proof steps and between +values in some error messages. 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 @@ -665,15 +666,24 @@ new, no line of old text is shown for them. .. image:: ../_static/diffs-coqtop-on3.png :alt: coqtop with Set Diffs on +This image shows an error message with diff highlighting in CoqIDE: + +.. + + .. image:: ../_static/diffs-error-message.png + :alt: |CoqIDE| error message with diffs + How to enable diffs ``````````````````` .. opt:: Diffs %( "on" %| "off" %| "removed" %) :name: Diffs - The “on” option highlights added tokens in green, while the “removed” option + The “on” setting highlights added tokens in green, while the “removed” setting additionally reprints items with removed tokens in red. Unchanged tokens in - modified items are shown with pale green or red. (Colors are user-configurable.) + modified items are shown with pale green or red. Diffs in error messages + use red and green for the compared values; they appear regardless of the setting. + (Colors are user-configurable.) For coqtop, showing diffs can be enabled when starting coqtop with the ``-diffs on|off|removed`` command-line option or by setting the :opt:`Diffs` option |
