diff options
| -rw-r--r-- | isa/isa.el | 28 | ||||
| -rw-r--r-- | isa/thy-mode.el | 2 |
2 files changed, 16 insertions, 14 deletions
@@ -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) |