From 803329b20efc58bc17bde2c65c95ad0279a6da22 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Thu, 10 Dec 1998 10:56:18 +0000 Subject: Fix for splash hack for theory files when proo-splash-inhibit=t. --- isa/example.ML | 1 - isa/isa.el | 3 ++- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/isa/example.ML b/isa/example.ML index 11b807f4..a8922e87 100644 --- a/isa/example.ML +++ b/isa/example.ML @@ -14,7 +14,6 @@ br conjI 1; be conjE 1; ba 1; be conjE 1; -ba 45; ba 1; qed "and_comms"; diff --git a/isa/isa.el b/isa/isa.el index f5d6158f..960d2730 100644 --- a/isa/isa.el +++ b/isa/isa.el @@ -343,7 +343,8 @@ isa-proofscript-mode." (string-match ".thy" (buffer-file-name))) (thy-mode) ;; Hack for splash screen - (if (memq 'proof-splash-timeout-waiter proof-mode-hook) + (if (and proof-mode-hook + (memq 'proof-splash-timeout-waiter proof-mode-hook)) (proof-splash-timeout-waiter)) ;; Has this theory file already been loaded by Isabelle? ;; Colour it blue if so. -- cgit v1.2.3