diff options
| author | Jim Fehrle | 2019-04-28 12:04:54 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2019-05-16 20:33:41 -0700 |
| commit | 9b41ff4e90a0303d9caf6e7e2f951a5046ce2d13 (patch) | |
| tree | e60ab950f28d2055949f4c9761a09d9030e67797 /generic | |
| parent | 09e099f44b0dc242367eb19d584b941a6dc0de09 (diff) | |
Highlight diffs in goals and some error messages
using Coq's proof diffs feature.
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/pg-goals.el | 3 | ||||
| -rw-r--r-- | generic/pg-response.el | 5 | ||||
| -rw-r--r-- | generic/proof-menu.el | 1 |
3 files changed, 7 insertions, 2 deletions
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)) |