FSF Emacs fix for buffer-file-truename, which is the

*abbreviated* form of file-truename!

4 files changed, 20 insertions, 7 deletions

diff --git a/generic/proof-script.el b/generic/proof-script.el
index 59350fc9..1a96b484 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1624,8 +1624,12 @@ Otherwise just do proof-restart-buffers to delete some spans from memory."
   "Finish setup of Proof General scripting mode.
 Call this function in the derived mode for the proof assistant to
 finish setup which depends on specific proof assistant configuration."
-    ;; Has buffer already been processed?
-  (and (member buffer-file-truename proof-included-files-list)
+  ;; Has buffer already been processed?
+  ;; NB: call to file-truename is needed for FSF Emacs which
+  ;; chooses to make buffer-file-truename abbreviate-file-name
+  ;; form of file-truename.
+  (and (member (file-truename buffer-file-truename)
+	       proof-included-files-list)
        (proof-mark-buffer-atomic (current-buffer)))
 
   ;; calculate some strings and regexps for searching
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index facf8700..78b710da 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -447,7 +447,10 @@ If FORCE, override proof-shell-erase-response-flag."
   (if (or proof-shell-erase-response-flag force)
       (if clean-windows
 	  (proof-clean-buffer proof-response-buffer)
-	(erase-buffer proof-response-buffer)))
+	;; NB: useful optional arg to erase buffer is XEmacs specific, 8-(.
+	;; (erase-buffer proof-response-buffer)
+	(with-current-buffer proof-response-buffer
+	  (erase-buffer))))
   (setq proof-shell-erase-response-flag erase-next-time))
 		  
 
diff --git a/generic/proof.el b/generic/proof.el
index 68560e0d..42d3b60c 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -189,9 +189,11 @@ Also ensures that point is visible."
   "Erase buffer and hide from display if proof-auto-delete-windows set.
 Auto deletion only affects selected frame.  (We assume that the selected
 frame is the one showing the script buffer.)"
-  (erase-buffer buffer)
-  (if proof-auto-delete-windows
-      (delete-windows-on buffer t)))
+  (with-current-buffer buffer
+    ;; NB: useful optional arg to erase buffer is XEmacs specific, 8-(.
+    (erase-buffer)
+    (if proof-auto-delete-windows
+	(delete-windows-on buffer t))))
 
 ;; utility function
 ;; FIXME da: maybe not used.  Put into spare parts file.
diff --git a/isa/isa.el b/isa/isa.el
index e25692c7..2b87a5ac 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -340,7 +340,11 @@ isa-proofscript-mode."
 	(proof-splash-timeout-waiter))
     ;; Has this theory file already been loaded by Isabelle?
     ;; Colour it blue if so.  
-    (and (member buffer-file-truename proof-included-files-list)
+    ;; NB: call to file-truename is needed for FSF Emacs which
+    ;; chooses to make buffer-file-truename abbreviate-file-name
+    ;; form of file-truename.
+    (and (member (file-truename buffer-file-truename)
+		 proof-included-files-list)
 	 (proof-mark-buffer-atomic (current-buffer)))
     )
    (t