From ce2f6526eff00bf01ba2e8ceb9ed3fc8966705be Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Mon, 26 Oct 1998 14:06:22 +0000 Subject: Fix buglet for when script buffer has no filename. --- isa/isa.el | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) (limited to 'isa/isa.el') 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 -- cgit v1.2.3