diff options
| author | Jim Fehrle | 2019-05-15 13:08:02 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2019-05-16 20:33:55 -0700 |
| commit | 7501326a228a5d0af1ad1d5bef4e8640cbd1e43f (patch) | |
| tree | edb7d34a298c1b82db38c92b48920763e5d6ecf8 | |
| parent | d8b501a5caf50ede62631e3fa30aa89f53db045f (diff) | |
Do a "Set Diffs" whenever backtracking. This also re-prints the
context (with diff annotations when enabled).
| -rw-r--r-- | coq/coq.el | 3 | ||||
| -rw-r--r-- | doc/ProofGeneral.texi | 6 |
2 files changed, 5 insertions, 4 deletions
@@ -1216,7 +1216,8 @@ be called and no command will be sent to Coq." (> (length (coq-get-span-proofstack (proof-last-locked-span))) ;; the number of aborts is the third arg of Backtrack. (string-to-number (match-string 1 cmd))))) - (list "Unset Silent." "Show.")) + ; "Set Diffs" always re-prints the proof context with (if enabled) diffs + (list "Unset Silent." (if (coq--post-v810) (coq-diffs) "Show."))) ((or ;; If we go back in the buffer and not in the above case, then only Unset ;; silent (there is no goal to show). diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 73bb98e5..ec449cc0 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -5226,9 +5226,9 @@ select @code{Coq -> Settings -> Save Settings}. The colors used to highlight diffs are configurable in the @code{Proof-General -> Advanced -> Customize -> Proof Faces} menu. -The 4 @code{Coq Diffs ...} faces control the highlights. Any line that -has added or removed tokens are shown with the entire line highlighted with -a @code{Bg} face. The added or removed tokens themselves are highlighted +The 4 @code{Coq Diffs ...} faces control the highlights. Lines that +have added or removed tokens are shown with the entire line highlighted with +a @code{Coq Diffs ... Bg} face. The added or removed tokens themselves are highlighted with non-@code{Bg} faces. @c ================================================================= |