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

*abbreviated* form of file-truename!

1 files changed, 5 insertions, 1 deletions

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