diff options
| author | Pierre Courtieu | 2019-06-06 11:33:33 +0200 |
|---|---|---|
| committer | GitHub | 2019-06-06 11:33:33 +0200 |
| commit | 89a6166a2ee61ff9cc84ccffe681a275c64c6856 (patch) | |
| tree | c9885900631fddc3fa1e2f78adfe9bfbce5b748b /generic | |
| parent | 9ebfbb6abbd5480b434ceadebec824d7c8804e73 (diff) | |
| parent | 7f1821cee8801a0f248aef492b9c1541e85a4880 (diff) | |
Merge pull request #426 from jfehrle/tweak
Proof diffs revisions requested by @monnier
Diffstat (limited to 'generic')
| -rwxr-xr-x[-rw-r--r--] | generic/pg-goals.el | 8 | ||||
| -rw-r--r-- | generic/pg-response.el | 9 |
2 files changed, 4 insertions, 13 deletions
diff --git a/generic/pg-goals.el b/generic/pg-goals.el index 2474c402..d0897fbe 100644..100755 --- a/generic/pg-goals.el +++ b/generic/pg-goals.el @@ -26,12 +26,6 @@ (require 'pg-assoc) -;; FIXME: This is required for `coq-insert-tagged-text', but we should never -;; use Coq-specific code from a generic/*.el file. Actually, this `require' -;; should fail if we're using PG with something else than Coq because the -;; coq/ subdir won't be in `load-path'! -(require 'coq-diffs) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; Goals buffer mode @@ -114,7 +108,7 @@ so the response buffer should not be cleared." ;; Only display if string is non-empty. (unless (string-equal string "") - (coq-insert-tagged-text string)) + (funcall pg-insert-text-function string)) (setq buffer-read-only t) (set-buffer-modified-p nil) diff --git a/generic/pg-response.el b/generic/pg-response.el index e94e710b..37f629af 100644 --- a/generic/pg-response.el +++ b/generic/pg-response.el @@ -31,11 +31,8 @@ (require 'pg-assoc) (require 'span) -;; FIXME: This is required for `coq-insert-tagged-text', but we should never -;; use Coq-specific code from a generic/*.el file. Actually, this `require' -;; should fail if we're using PG with something else than Coq because the -;; coq/ subdir won't be in `load-path'! -(require 'coq-diffs) +(defvar pg-insert-text-function #'insert + "hook for coq diffs highlighting routine") ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -415,7 +412,7 @@ Returns non-nil if response buffer was cleared." (let ((start (point))) (if face (insert str) - (coq-insert-tagged-text str)) + (funcall pg-insert-text-function str)) (unless (bolp) (newline)) (when face ;; FIXME: Why not (put-text-property start (point) 'face face)? |