Add hook for coq diff-highlighting routine

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..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)?