diff options
| author | Emilio Jesus Gallego Arias | 2019-03-20 02:21:14 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-03-20 02:21:14 +0100 |
| commit | e5a2f0452cf9523bc86e71ae6d2ac30883a28be6 (patch) | |
| tree | 91492ff7e20a3ad53c42257e04e0a0f44909ed42 /doc | |
| parent | 9681f4bd4e184e3d748c4539667460537b55429f (diff) | |
| parent | ef2fce93057484b015c85713ad83f53f88762271 (diff) | |
Merge PR #8669: Show diffs in some error messages
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: jfehrle
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 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 |
