diff options
| -rw-r--r-- | generic/proof-splash.el | 15 | ||||
| -rw-r--r-- | isa/isa.el | 13 |
2 files changed, 22 insertions, 6 deletions
diff --git a/generic/proof-splash.el b/generic/proof-splash.el index 025431d6..110b4b71 100644 --- a/generic/proof-splash.el +++ b/generic/proof-splash.el @@ -45,6 +45,13 @@ Gif filename depends on colour depth of display." :type 'boolean :group 'proof) +(defcustom proof-splash-extensions nil + "*Prover specific extensions of splash screen. +These are evaluated and appended to proof-splash-contents, which see." + :type 'sexp + :group 'proof-config) + + (defcustom proof-splash-contents (list nil @@ -57,12 +64,12 @@ Gif filename depends on colour depth of display." "Welcome to" (concat proof-assistant " Proof General!") nil) - "*List defining splash screen displayed when Proof General is started. + "List defining splash screen displayed when Proof General is started. If an element is a string or an image specifier, it is displayed centred on the window on its own line. If it is nil, a new line is inserted." :type 'sexp - :group 'proof-config) + :group 'proof-general-internals) (defcustom proof-splash-time 1.5 "Minimum number of seconds to display splash screen for. @@ -122,7 +129,9 @@ Only do it if proof-splash-display is nil." ((winconf (current-window-configuration)) (splashbuf (get-buffer-create proof-splash-welcome)) (after-change-functions nil) ; no font-lock, thank you - (splash-contents proof-splash-contents) + (splash-contents (append + proof-splash-contents + (eval proof-splash-extensions))) s) (with-current-buffer splashbuf (erase-buffer) @@ -10,6 +10,13 @@ (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)))) (require 'proof) (require 'isa-syntax) @@ -71,9 +78,9 @@ no regular or easily discernable structure." ;;; End of a command needs parsing to find, so this is approximate. (defvar isa-outline-heading-end-regexp ";[ \t\n]*") -;; -(defvar isa-shell-outline-regexp isa-goal-regexp) -(defvar isa-shell-outline-heading-end-regexp isa-goal-regexp) +;; FIXME: not sure about this one +(defvar isa-shell-outline-regexp "\370[ \t]*\\([0-9]+\\)\\.") +(defvar isa-shell-outline-heading-end-regexp "$") ;;; ---- end-outline |