diff options
| -rw-r--r-- | CHANGES | 8 | ||||
| -rw-r--r-- | coq/coq-abbrev.el | 16 | ||||
| -rw-r--r-- | coq/coq-db.el | 27 | ||||
| -rw-r--r-- | coq/coq-diffs.el | 65 | ||||
| -rw-r--r-- | coq/coq.el | 30 | ||||
| -rw-r--r-- | doc/ProofGeneral.texi | 40 | ||||
| -rw-r--r-- | generic/pg-goals.el | 3 | ||||
| -rw-r--r-- | generic/pg-response.el | 5 | ||||
| -rw-r--r-- | generic/proof-menu.el | 1 |
9 files changed, 189 insertions, 6 deletions
@@ -75,7 +75,6 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac Hide/ unhide status remains when goal changes. - *** Highlighting of hypothesis You can highlight hypothesis in goals buffer on a per name @@ -84,8 +83,7 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac Highlighting status remains when goal changes. - -**** Automtic highlighting with (search)About. +**** Automatic highlighting with (search)About. Hypothesis cited in the response buffer after C-c C-a C-a (i.e. M-x coq-SearchAbout) will be highlighted automatically. Any other hypothesis highlighted is unhighlighted. @@ -94,6 +92,10 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac (setq coq-highlight-hyps-cited-in-response nil) +*** Support Coq's feature for highlighting the differences + between successive proof steps. See section 11.8 ("Showing + Proof Diffs") in the documentation. + *** bug fixes - avoid leaving partial files behind when compilation fails - 123: Parallel background compliation fails to execute some diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 4d2d2d0e..391b1238 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -220,6 +220,22 @@ :active (and coq-compile-before-require coq-compile-parallel-in-background) :help "Abort background compilation and kill all compilation processes."]) + ("Diffs" + ["off" + (customize-set-variable 'coq-diffs 'off) + :style radio + :selected (eq coq-diffs 'off) + :help "Don't show diffs"] + ["on" + (customize-set-variable 'coq-diffs 'on) + :style radio + :selected (eq coq-diffs 'on) + :help "Show diffs: only added"] + ["removed" + (customize-set-variable 'coq-diffs 'removed) + :style radio + :selected (eq coq-diffs 'removed) + :help "Show diffs: added and removed"]) "" ["Print..." coq-Print :help "With prefix arg (C-u): Set Printing All first"] ["Check..." coq-Check :help "With prefix arg (C-u): Set Printing All first"] diff --git a/coq/coq-db.el b/coq/coq-db.el index b01e8018..758177c9 100644 --- a/coq/coq-db.el +++ b/coq/coq-db.el @@ -26,6 +26,7 @@ (eval-when-compile (require 'cl-lib)) ;decf (require 'holes) +(require 'diff-mode) (defconst coq-syntax-db nil "Documentation-only variable, for coq keyword databases. @@ -365,6 +366,32 @@ Required so that 'coq-symbol-binder-face is a proper facename") (defconst coq-question-mark-face 'coq-question-mark-face) +(defface coq-diffs-added-face + '((t . (:inherit diff-refine-added))) + "Face used to highlight added text in diffs" + :group 'proof-faces) + +(defface coq-diffs-removed-face + '((t . (:inherit diff-refine-removed))) + "Face used to highlight removed text in diffs" + :group 'proof-faces) + +(defface coq-diffs-added-bg-face + '((t . (:inherit diff-added))) + "Face used to highlight unchanged text in lines showing added text in diffs" + :group 'proof-faces) + +(defface coq-diffs-removed-bg-face + '((t . (:inherit diff-removed))) + "Face used to highlight unchanged text in lines showing removed text in diffs" + :group 'proof-faces) + +(defvar coq-tag-map + '(("diff.added" . coq-diffs-added-face) + ("diff.removed" . coq-diffs-removed-face) + ("diff.added.bg" . coq-diffs-added-bg-face) + ("diff.removed.bg" . coq-diffs-removed-bg-face))) + (provide 'coq-db) ;;; coq-db.el ends here diff --git a/coq/coq-diffs.el b/coq/coq-diffs.el new file mode 100644 index 00000000..d93adf73 --- /dev/null +++ b/coq/coq-diffs.el @@ -0,0 +1,65 @@ +;;; coq-diffs.el --- highlight text marked with XML-like tags for Coq diffs + +;; This file is part of Proof General. + +;; Portions © Copyright 2019 Jim Fehrle + +;; Author: Jim Fehrle <jim.fehrle@gmail.com> + +;; License: BSD-3 (3-Clause BSD License) + +;;; Commentary: +;; + +(require 'coq-db) + +;;; Code: + +(defun coq-insert-with-face (str face) + (let ((start (point))) + (insert str) + (if face + (overlay-put (span-make start (point-max)) 'face face)))) + +(defun coq-insert-tagged-text (str) +"Insert text into the current buffer applying faces specified by tags. + +For example '<diff.added>foo</diff.added>' inserts 'foo' in the buffer +and applies the appropriate face. + +coq-tag-map defines the mapping from tag name to face." + (let* ((len (length str)) + (off 0) + (fstack) + (rhs)) + (while (< off len) + (string-match "^\\([ \t]*\\)\\(.*\n?\\)" str off) + (setq off (match-end 0)) + (coq-insert-with-face (match-string 1 str) nil) ;; begin-line white space + (setq rhs (match-string 2 str)) + (string-match "[ \t\n]*$" rhs) + (let* ((end-white (match-string 0 rhs)) ;; end-line white space + (line (substring rhs 0 (- (length rhs) (length end-white)))) + (llen (length line)) + (loff 0)) + (while (< loff llen) + (if (> loff 0) + (aset line (1- loff) ?\n)) ;; only way to get an anchored search midstring + (cond + ; make sure that a) the matched string is never the empty string, and + ; b) that every non-empty string has a match + ((string-match "^<\\(/?\\)\\([a-zA-Z\\.]+\\)>" line loff) ;; tag + (let* ((end-mark (match-string 1 line)) + (tag (match-string 2 line)) + (face (cdr (assoc tag coq-tag-map)))) + (if face + (setq fstack (if (equal end-mark "") (cons face fstack) (cdr fstack))) + (coq-insert-with-face (match-string 0 line) (car fstack))))) ;; unknown tag, show as-is + ((string-match "^<?[^<\n]+" line loff) ;; text + (coq-insert-with-face (match-string 0 line) (car fstack)))) + (setq loff (match-end 0))) + (coq-insert-with-face end-white nil))))) ; end-line white space + +(provide 'coq-diffs) + +;;; coq-diffs.el ends here @@ -1891,7 +1891,7 @@ See `coq-fold-hyp'." ;; type. (setq proof-assistant-additional-settings '(coq-compile-quick coq-compile-keep-going - coq-compile-auto-save coq-lock-ancestors)) + coq-compile-auto-save coq-lock-ancestors coq-diffs)) (setq proof-goal-command-p #'coq-goal-command-p proof-find-and-forget-fn #'coq-find-and-forget @@ -2070,6 +2070,34 @@ See `coq-fold-hyp'." :type 'integer :setting "Set Printing Depth %i . ") +(defun coq-diffs () + "Return string for setting Coq Diffs. +Return the empty string if the version of Coq < 8.10." + (if (coq--post-v810) + (format "Set Diffs \"%s\". " (symbol-name coq-diffs)) + "")) + +(defun coq-diffs--setter (symbol new-value) + ":set function fo `coq-diffs'. +Set Diffs setting if Coq is running and has a version >= 8.10." + (set symbol new-value) + (if (proof-shell-available-p) + (let ((cmd (coq-diffs))) + (if (equal cmd "") + (message "Ignore coq-diffs setting %s for Coq before 8.10" + (symbol-name coq-diffs)) + (proof-shell-invisible-command cmd))))) + +(defcustom coq-diffs 'off + "Controls Coq Diffs option" + :type '(radio + (const :tag "Don't show diffs" off) + (const :tag "Show diffs: only added" on) + (const :tag "Show diffs: added and removed" removed)) + :safe (lambda (v) (member v '(off on removed))) + :set 'coq-diffs--setter + :group 'coq) + ;; Obsolete: ;;(defpacustom undo-depth coq-default-undo-limit ;; "Depth of undo history. Undo behaviour will break beyond this size." diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index b3026608..73bb98e5 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -4302,6 +4302,7 @@ assistant. It supports most of the generic features of Proof General. * User-loaded tactics:: * Holes feature:: * Proof-Tree Visualization:: +* Showing Proof Diffs:: @end menu @@ -5190,6 +5191,45 @@ To support @code{Grab Existential Variables} Prooftree can actually display several graphically independent proof trees in several layers. +@node Showing Proof Diffs +@section Showing Proof Diffs + +Coq 8.10 supports automatically highlighting the differences +between successive proof steps in Proof General. The feature is described in the +@uref{https://coq.inria.fr/distrib/current/refman/proof-engine/proof-handling.html#showing-differences-between-proof-steps, +Coq Documentation}. + +The Coq proof diff does more than a basic "diff" operation. For example: + +@itemize @bullet +@item diffs are computed on a per-token basis (as determined by the Coq lexer) rather + than on a per-character basis, probably a better match for how people understand + the output. (For example, a token-based diff between "abc" and "axc" will + highlight all of "abc" and "axc" as a difference, while a character-based diff + would indicate that "a" and "c" are in common and that only the "b"/"x" is a + difference.) +@item diffs ignore the order of hypotheses +@item tactics that only change the proof view are handled specially, for + example "swap" after a "split" will show the diffs between before "split" + and after "swap", which is more useful +@item some error messages have been instrumented to show diffs where it is helpful +@end itemize + +To enable or disable diffs, set @code{coq-diffs} (select menu @code{Coq -> Diffs}) +to "on", "off" or "removed". "on" highlights added tokens with the background +color from @code{diff-refine-added}. "removed" highlights removed tokens +with the background color from @code{diff-refine-removed}. With the "removed" setting, +lines that have both added and removed text may be shown twice, as "before" and +"after" lines. +To preserve the settings for the next time you start Proof General, +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 +with non-@code{Bg} faces. @c ================================================================= @c diff --git a/generic/pg-goals.el b/generic/pg-goals.el index 37862a64..a76fbb44 100644 --- a/generic/pg-goals.el +++ b/generic/pg-goals.el @@ -25,6 +25,7 @@ (defvar proof-assistant-menu) ; defined by macro in proof-menu (require 'pg-assoc) +(require 'coq-diffs) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; @@ -109,7 +110,7 @@ so the response buffer should not be cleared." ;; Only display if string is non-empty. (unless (string-equal string "") - (insert string)) + (coq-insert-tagged-text string)) (setq buffer-read-only t) (set-buffer-modified-p nil) diff --git a/generic/pg-response.el b/generic/pg-response.el index 650e83a0..5fadca99 100644 --- a/generic/pg-response.el +++ b/generic/pg-response.el @@ -30,6 +30,7 @@ (require 'pg-assoc) (require 'span) +(require 'coq-diffs) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -409,7 +410,9 @@ Returns non-nil if response buffer was cleared." (eq (point-min) (point-max))) (newline)) (setq start (point)) - (insert str) + (if face + (insert str) + (coq-insert-tagged-text str)) (unless (bolp) (newline)) (when face (overlay-put diff --git a/generic/proof-menu.el b/generic/proof-menu.el index 2900a6b1..ba3d05ff 100644 --- a/generic/proof-menu.el +++ b/generic/proof-menu.el @@ -860,6 +860,7 @@ KEY is the optional key binding." ["Save Settings" (proof-settings-save) (proof-settings-changed-from-saved-p)])) groups ents) + ; todo: AFAICT the following statement does nothing and can be removed (mapc (lambda (stg) (add-to-list 'groups (get (car stg) 'pggroup))) proof-assistant-settings) (dolist (grp (reverse groups)) |