* coq/coq-diffs.el (coq-insert-tagged-text): Rework to avoid `aset`

(coq-insert-with-face): Don't assume we're at EOB.

* generic/pg-goals.el (pg-goals-display): Use with-current-buffer.

* generic/pg-response.el (pg-response-maybe-erase): Narrow the scope of
inhibit-read-only.
(pg-response-display-with-face): Use `member`.  Remove unused var `end`.
Only bind `start` when we have a value for it.
(proof-trace-buffer-display): Use with-current-buffer.

1 files changed, 30 insertions, 25 deletions

diff --git a/coq/coq-diffs.el b/coq/coq-diffs.el
index d93adf73..7d5e8f58 100644
--- a/coq/coq-diffs.el
+++ b/coq/coq-diffs.el
@@ -19,46 +19,51 @@
   (let ((start (point)))
     (insert str)
     (if face
-      (overlay-put (span-make start (point-max)) 'face face))))
+        ;; FIXME: Why not (put-text-property start (point) 'face face)?
+        (overlay-put (span-make start (point)) 'face face))))
 
 (defun coq-insert-tagged-text (str)
-"Insert text into the current buffer applying faces specified by tags.
+  "Insert text into the current buffer applying faces specified by tags.
 
 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-tag-map' defines the mapping from tag name to face."
   (let* ((len (length str))
          (off 0)
-	     (fstack)
-	     (rhs))
+	 (fstack)
+	 (rhs))
+    ;; FIXME: It would likely be better to insert `str' into the buffer
+    ;; and then work in the buffer instead of manipulating strings.
     (while (< off len)
       (string-match "^\\([ \t]*\\)\\(.*\n?\\)" str off)
       (setq off (match-end 0))
-      (coq-insert-with-face (match-string 1 str) nil)  ;; begin-line white space
+      ;; FIXME: Why handle whitespace specially?
+      (insert (match-string 1 str)) ;; begin-line white space
       (setq rhs (match-string 2 str))
-      (string-match "[ \t\n]*$" rhs)
-      (let* ((end-white (match-string 0 rhs))  ;; end-line white space
+      ;; 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))
-        (while (< loff llen)
-          (if (> loff 0)
-            (aset line (1- loff) ?\n))   ;; only way to get an anchored search midstring
-          (cond
-            ; make sure that a) the matched string is never the empty string, and
-            ; b) that every non-empty string has a match
-            ((string-match "^<\\(/?\\)\\([a-zA-Z\\.]+\\)>" line loff)    ;; tag
-              (let* ((end-mark (match-string 1 line))
-                     (tag (match-string 2 line))
-                     (face (cdr (assoc tag coq-tag-map))))
-                (if face
-                  (setq fstack (if (equal end-mark "") (cons face fstack) (cdr fstack)))
-                  (coq-insert-with-face (match-string 0 line) (car fstack)))))    ;; unknown tag, show as-is
-            ((string-match "^<?[^<\n]+" line loff)    ;; text
-              (coq-insert-with-face (match-string 0 line) (car fstack))))
-          (setq loff (match-end 0)))
-        (coq-insert-with-face end-white nil)))))    ; end-line white space
+        ;; 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))
+                 (tag (match-string 2 line))
+                 (face (cdr (assoc tag coq-tag-map)))
+                 (start (match-beginning 0))
+                 (end (match-end 0)))
+            (coq-insert-with-face (substring line loff start) (car fstack))
+            (setq loff end)
+            (if face
+                (setq fstack (if end-mark (cdr fstack) (cons face fstack)))
+              ;; Unknown tag, show as-is!
+              (coq-insert-with-face (substring line start end) (car fstack)))))
+        (coq-insert-with-face (substring line loff) (car fstack))
+        (insert end-white)))))    ; end-line white space
 
 (provide 'coq-diffs)