diff options
| author | Jim Fehrle | 2018-10-07 15:14:56 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2019-02-28 15:39:08 -0800 |
| commit | ef2fce93057484b015c85713ad83f53f88762271 (patch) | |
| tree | 9d7f73ebe0fa75e91855099465f3c3469cbe27ca /doc | |
| parent | 9736f255287a7207d00422b06de802d62b8304fe (diff) | |
Show diffs in error messages if color is enabled
Diffstat (limited to 'doc')
| -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 2300a317f1..d0bd9e396d 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 |
