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

2 files changed, 53 insertions, 47 deletions

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