Fix buglet for when script buffer has no filename.

1 files changed, 8 insertions, 3 deletions

diff --git a/isa/isa.el b/isa/isa.el
index cc189c67..a848ab46 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -160,6 +160,9 @@ no regular or easily discernable structure."
 ;; Unfortunately, use_thy_no_topml followed by update(); doesn't work
 ;; for *theory* files, because update() will report that the ML file
 
+;; Unfortunately, use_thy_no_topml followed by update(); doesn't work
+;; for *theory* files, because update() will report that the ML file
+;; 
 (defconst isa-usethy-command "use_thy \"%s\"; update();"
   "Command to send to Isabelle to process a theory file.")
 
@@ -244,15 +247,17 @@ Files with extension .thy will be in thy-mode, otherwise we choose
 isa-proofscript-mode."
   (interactive)
   (cond
-   ((string-match ".thy" (buffer-file-name))
+   (;; Theory files only if they have the right extension
+    (and (buffer-file-name)
+	 (string-match ".thy" (buffer-file-name)))
     (thy-mode)
-    ;; Has this theory file been loaded by Isabelle?
+    ;; Has this theory file already been loaded by Isabelle?
     ;; Colour it blue if so.  
     (and (member buffer-file-truename proof-included-files-list)
 	 (proof-mark-buffer-atomic (current-buffer)))
     )
    (t 
-    ;; Proof mode does this automatically.
+    ;; Proof mode does that automatically.
     (isa-proofscript-mode))))
 
 (eval-after-load