* 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.

3 files changed, 83 insertions, 72 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)
 
diff --git a/generic/pg-goals.el b/generic/pg-goals.el
index a76fbb44..3efc7bd7 100644
--- a/generic/pg-goals.el
+++ b/generic/pg-goals.el
@@ -3,7 +3,7 @@
 ;; This file is part of Proof General.
 
 ;; Portions © Copyright 1994-2012  David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003-2018  Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2019  Free Software Foundation, Inc.
 ;; Portions © Copyright 2001-2017  Pierre Courtieu
 ;; Portions © Copyright 2010, 2016  Erik Martin-Dorel
 ;; Portions © Copyright 2011-2013, 2016-2017  Hendrik Tews
@@ -25,7 +25,12 @@
 (defvar proof-assistant-menu)           ; defined by macro in proof-menu
 
 (require 'pg-assoc)
-(require 'coq-diffs)
+
+;; 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)h
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
@@ -92,16 +97,15 @@ If KEEPRESPONSE is non-nil, we assume that a response message
 corresponding to this goals message has already been displayed
 before this goals message (see `proof-shell-handle-delayed-output'),
 so the response buffer should not be cleared."
-  (save-excursion
-    ;; Response buffer may be out of date. It may contain (error)
-    ;; messages relating to earlier proof states
+  ;; Response buffer may be out of date. It may contain (error)
+  ;; messages relating to earlier proof states
 
-    ;; Erase the response buffer if need be, maybe removing the
-    ;; window.  Indicate it should be erased before the next output.
-    (pg-response-maybe-erase t t nil keepresponse)
+  ;; Erase the response buffer if need be, maybe removing the
+  ;; window.  Indicate it should be erased before the next output.
+  (pg-response-maybe-erase t t nil keepresponse)
 
-    ;; Erase the goals buffer and add in the new string
-    (set-buffer proof-goals-buffer)
+  ;; Erase the goals buffer and add in the new string
+  (with-current-buffer proof-goals-buffer
 
     (setq buffer-read-only nil)
 
diff --git a/generic/pg-response.el b/generic/pg-response.el
index 5fadca99..e94e710b 100644
--- a/generic/pg-response.el
+++ b/generic/pg-response.el
@@ -3,7 +3,7 @@
 ;; This file is part of Proof General.
 
 ;; Portions © Copyright 1994-2012  David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003-2018  Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2019  Free Software Foundation, Inc.
 ;; Portions © Copyright 2001-2017  Pierre Courtieu
 ;; Portions © Copyright 2010, 2016  Erik Martin-Dorel
 ;; Portions © Copyright 2011-2013, 2016-2017  Hendrik Tews
@@ -30,6 +30,11 @@
 
 (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)
 
 
@@ -348,8 +353,7 @@ will never be cleared unless FORCE is set.
 No effect if there is no response buffer currently.
 Returns non-nil if response buffer was cleared."
   (when (buffer-live-p proof-response-buffer)
-    (let ((inhibit-read-only t)
-	  (doit (or (and
+    (let ((doit (or (and
 		     proof-tidy-response
 		     (not keep)
 		     (not (eq pg-response-erase-flag 'invisible))
@@ -359,10 +363,11 @@ Returns non-nil if response buffer was cleared."
 	  (if clean-windows
 	      (proof-clean-buffer proof-response-buffer)
 	    (with-current-buffer proof-response-buffer
-	      (setq pg-response-next-error nil)	; all error msgs lost!
-	      (if (> (buffer-size) 0)
-		  (bufhist-checkpoint-and-erase))
-	      (set-buffer-modified-p nil))))
+              (let ((inhibit-read-only t))
+	        (setq pg-response-next-error nil) ; all error msgs lost!
+	        (if (> (buffer-size) 0)
+		    (bufhist-checkpoint-and-erase))
+	        (set-buffer-modified-p nil)))))
       (setq pg-response-erase-flag erase-next-time)
       doit)))
 
@@ -394,29 +399,28 @@ Returns non-nil if response buffer was cleared."
 (defun pg-response-display-with-face (str &optional face)
   "Display STR with FACE in response buffer."
   (cond
-   ((string-equal str ""))
-   ((string-equal str "\n"))		; quick exit, no display.
+   ((member str '("" "\n")))		; Quick exit, no display.
    (t
-    (let (start end)
-      (with-current-buffer proof-response-buffer
-        (setq buffer-read-only nil)
-        ;; da: I've moved newline before the string itself, to match
-        ;; the other cases when messages are inserted and to cope
-        ;; with warnings after delayed output (non newline terminated).
-        (goto-char (point-max))
-        ;; insert a newline before the new message unless the
-        ;; buffer is empty or proof-script-insert-newlines is nil
-        (unless (or (not proof-script-insert-newlines)
-                    (eq (point-min) (point-max)))
-          (newline))
-        (setq start (point))
+    (with-current-buffer proof-response-buffer
+      (setq buffer-read-only nil)
+      ;; da: I've moved newline before the string itself, to match
+      ;; the other cases when messages are inserted and to cope
+      ;; with warnings after delayed output (non newline terminated).
+      (goto-char (point-max))
+      ;; insert a newline before the new message unless the
+      ;; buffer is empty or proof-script-insert-newlines is nil
+      (unless (or (not proof-script-insert-newlines)
+                  (bobp))               ;FIXME: Why not `bolp'?
+        (newline))
+      (let ((start (point)))
         (if face
-          (insert str)
+            (insert str)
           (coq-insert-tagged-text str))
         (unless (bolp) (newline))
         (when face
+          ;; FIXME: Why not (put-text-property start (point) 'face face)?
           (overlay-put
-           (span-make start (point-max))
+           (span-make start (point))
            'face face))
 
 	(setq buffer-read-only t)
@@ -566,17 +570,15 @@ A value of 0 stands for unbounded."
 ;; An analogue of pg-response-display-with-face
 (defun proof-trace-buffer-display (start end)
   "Copy region START END from current buffer to end of the trace buffer."
-  (let ((cbuf   (current-buffer))
-	(nbuf   proof-trace-buffer))
-    (set-buffer nbuf)
-    (save-excursion
-      (goto-char (point-max))
-      (let ((inhibit-read-only t))
-	(insert ?\n)
-	(insert-buffer-substring cbuf start end)
-	(unless (bolp)
-	  (insert ?\n))))
-    (set-buffer cbuf)))
+  (let ((cbuf   (current-buffer)))
+    (with-current-buffer proof-trace-buffer
+      (save-excursion
+        (goto-char (point-max))
+        (let ((inhibit-read-only t))
+	  (insert ?\n)
+	  (insert-buffer-substring cbuf start end)
+	  (unless (bolp)
+	    (insert ?\n)))))))
 
 (defun proof-trace-buffer-finish ()
   "Call to complete a batch of tracing output.
@@ -608,8 +610,8 @@ The buffer is truncated if its size is greater than `proof-trace-buffer-max-line
     (let (start str)
       (goto-char (point-max))
       (newline)
-      (setq start (point))
-      (insert str)
+      (setq start (point))              ;FIXME: Unused!
+      (insert str)                      ;FIXME: `str' is nil!!!
       (unless (bolp) (newline))
       (set-buffer-modified-p nil))))