Disabled problematic requires temporarily.

2 files changed, 16 insertions, 14 deletions

diff --git a/isa/isa.el b/isa/isa.el
index 292f6095..d4ce4161 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -9,28 +9,30 @@
 ;;
 
 
-(eval-when-compile
-  (require 'proof-config))
+
+
+;; FIXME: this most be done before loading proof-config, shame.
+(setq proof-tags-support nil) ; we don't want it, no isatags prog. 
 
 ;; Add Isabelle image onto splash screen
 (custom-set-variables
  '(proof-splash-extensions
-   (list
-    nil
-    (proof-splash-display-image "isabelle_transparent" t))))
-(custom-set-variables
- '(proof-tags-support nil))  ; we don't want it, no isatags prog.
+   '(list
+     nil
+     (proof-splash-display-image "isabelle_transparent" t))))
 
 (require 'proof)
 (require 'isa-syntax)
 
 ;; To make byte compiler be quiet.
-(eval-when-compile
-  (require 'proof-shell)
-  (require 'proof-script)
-  (require 'outline)
-  (cond ((fboundp 'make-extent) (require 'span-extent))
-	((fboundp 'make-overlay) (require 'span-overlay))))
+;; NASTY: these result in loads when evaluated 
+;; ordinarily (from non-byte compiled code).
+;(eval-when-compile
+;  (require 'proof-script)
+;  (require 'proof-shell)
+;  (require 'outline)
+;  (cond ((fboundp 'make-extent) (require 'span-extent))
+;	((fboundp 'make-overlay) (require 'span-overlay))))
 
 
 
diff --git a/isa/thy-mode.el b/isa/thy-mode.el
index 948f29e0..c623b078 100644
--- a/isa/thy-mode.el
+++ b/isa/thy-mode.el
@@ -32,7 +32,7 @@ any of the usual bracket characters in unusual ways."
   :type 'boolean
   :group 'thy)
 
-(defcustom thy-use-sml-mode isabelle-use-sml-mode
+(defcustom thy-use-sml-mode nil
   "*If non-nil, invoke sml-mode inside \"ML\" section of theory files."
   :type 'boolean
   :group 'thy)