Add hook for coq diff-highlighting routine

4 files changed, 17 insertions, 17 deletions

diff --git a/coq/coq-diffs.el b/coq/coq-diffs.el
index 7d5e8f58..67d2fcc7 100644
--- a/coq/coq-diffs.el
+++ b/coq/coq-diffs.el
@@ -29,6 +29,14 @@ 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."
+;; Coq inserts tags before splitting into lines.  Avoid highlighting
+;; white space at the beginning or end of lines in a conclusion or
+;; hypothesis that's split across multiple lines.
+
+;; Doesn't handle the unlikely case of escaping regular text
+;; that looks like a tag.  Unknown tags such as "<foo>" are
+;; shown as-is.  The user can turn off diffs in this very unlikely case.
+
   (let* ((len (length str))
          (off 0)
 	 (fstack)
@@ -38,17 +46,13 @@ and applies the appropriate face.
     (while (< off len)
       (string-match "^\\([ \t]*\\)\\(.*\n?\\)" str off)
       (setq off (match-end 0))
-      ;; FIXME: Why handle whitespace specially?
       (insert (match-string 1 str)) ;; begin-line white space
       (setq rhs (match-string 2 str))
-      ;; FIXME: Why handle whitespace specially?
       (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))
-        ;; FIXME: I don't see any mechanism here to escape text, in case
-        ;; we need to include text that happen to look just like a tag!
         (while (and (< loff llen)
                     (string-match "<\\(/\\)?\\([a-zA-Z\\.]+\\)>" line loff))
           (let* ((end-mark (match-beginning 1))
diff --git a/coq/coq.el b/coq/coq.el
index 21b1acf9..0f6d6f84 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -58,6 +58,11 @@
 (require 'coq-abbrev)                   ; abbrev and coq specific menu
 (require 'coq-seq-compile)              ; sequential compilation of Requires
 (require 'coq-par-compile)              ; parallel compilation of Requires
+
+;; set hook for diff highlighting routine from non-Coq code
+(require 'coq-diffs)
+(setq pg-insert-text-function 'coq-insert-tagged-text)
+
 (defvar prettify-symbols-alist)
 
 
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)?