From 0afe38adf55608b26f04a77f312d4805ce568da6 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Fri, 31 May 2019 16:59:19 -0700
Subject: Add hook for coq diff-highlighting routine

---
 generic/pg-goals.el    | 8 +-------
 generic/pg-response.el | 9 +++------
 2 files changed, 4 insertions(+), 13 deletions(-)
 mode change 100644 => 100755 generic/pg-goals.el

(limited to 'generic')

diff --git a/generic/pg-goals.el b/generic/pg-goals.el
old mode 100644
new mode 100755
index 2474c402..d0897fbe
--- 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..7f36fc6f 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)
+;; hook for coq diffs highlighting routine
+(defvar pg-insert-text-function 'insert)
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -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)?
-- 
cgit v1.2.3