Separated splash screen code

2 files changed, 145 insertions, 148 deletions

diff --git a/generic/proof-splash.el b/generic/proof-splash.el
new file mode 100644
index 00000000..f3d0543a
--- /dev/null
+++ b/generic/proof-splash.el
@@ -0,0 +1,140 @@
+;; proof-splash.el -- Splash welcome screen for Proof General
+;;
+;; Copyright (C) 1998 LFCS Edinburgh. 
+;; Author: David Aspinall
+;; Maintainer:  Proof General maintainer <proofgen@dcs.ed.ac.uk>
+;;
+;; $Id$
+;;
+
+(require 'annotations)
+(defconst proof-welcome "*Proof General Welcome*"
+  "Name of the Proof General splash buffer.")
+
+(defconst proof-display-splash-image
+  ;; Use jpeg if we can, otherwise assume gif will work.
+  (if (featurep 'jpeg)
+      (cons 'jpeg
+	    (concat proof-internal-images-directory 
+		    "ProofGeneral.jpg"))
+  (cons 'gif
+	(concat proof-internal-images-directory 
+		(concat "ProofGeneral"
+			(or (and
+			     (fboundp 'device-pixel-depth)
+			     (> (device-pixel-depth) 8)
+			     ".gif")
+			    ;; Low colour gif for poor displays
+			    ".8bit.gif")))))
+  "Format and File name of Proof General Image.")
+
+(defcustom proof-display-splash 
+  (valid-instantiator-p
+   (vector (car proof-display-splash-image)
+		 :file (cdr proof-display-splash-image)) 'image)
+  "*Display splash screen when Proof General is loaded."
+  :type 'boolean
+  :group 'proof)
+
+(defcustom proof-internal-display-splash-time 4
+  "Minimum number of seconds to display splash screen for.
+If the machine gets to the end of proof-mode faster than this,
+we wait for the remaining time.  Must be a value less than 40."
+  :type 'integer
+  :group 'proof-internal)
+
+;; We take some care to preserve the users window configuration
+;; underneath the splash screen.  This is just to be polite.
+(defun proof-remove-splash-screen (conf)
+  "Make function to remove splash screen and restore window config to conf."
+  `(lambda ()
+     (and ;; If splash buffer is still alive 
+      (get-buffer proof-welcome)
+      (if (get-buffer-window (get-buffer proof-welcome))
+	  ;; Restore the window config if splash is being displayed
+	  (set-window-configuration ,conf)
+	t)
+      ;; And destroy splash buffer.
+      (kill-buffer proof-welcome))))
+
+(defun proof-display-splash-screen ()
+  "Save window config and display Proof General splash screen.
+No effect if proof-display-splash-time is zero."
+  (interactive)
+  (if proof-display-splash
+      (let*
+	  ((splashbuf   (get-buffer-create proof-welcome))
+	   (imglyph	(make-glyph
+			 (list (vector (car proof-display-splash-image) ':file
+				       (cdr proof-display-splash-image)))))
+	   ;; Keep win config explicitly instead of pushing/popping because
+	   ;; if the user switches windows by hand in some way, we want
+	   ;; to ignore the saved value.  Unfortunately there seems to
+	   ;; be no way currently to remove the top item of the stack.
+	   (removefn    (proof-remove-splash-screen
+			 (current-window-configuration))))
+	(save-excursion
+	  (set-buffer splashbuf)
+	  (erase-buffer)
+	  ;; FIXME: centre display better.  support FSFmacs.
+	  (insert "\n\n\n\t\t")
+	  (insert-char ?\  (/ (length proof-assistant) 2))
+	  (insert "    Welcome to\n\t\t  "
+		  proof-assistant " Proof General!\n\n\n\t\t ")
+	  (let ((ann (make-annotation imglyph))) ; reveal-annotation doesn't
+	    (reveal-annotation ann))	;      autoload, so use let form.  
+	  (insert "\n\n")
+	  (delete-other-windows (display-buffer splashbuf)))
+	;; Start the timer with a dummy value of 40 secs, to time the
+	;; loading of the rest of the mode.  This is a kludge to make
+	;; sure that the splash screen appears at least throughout the
+	;; load (which shouldn't last 40 secs!).  But if the load is
+	;; triggered by something other than a call to proof-mode,
+	;; the splash screen *will* appear for 40 secs (unless the
+	;; user kills it or switches buffer).
+	(redisplay-frame nil t)
+	(start-itimer proof-welcome removefn 40))))
+
+;; PROBLEM: when to call proof-display-splash-screen?  Effect we'd
+;; like is to call it during loading/initialising.  It's hard to make
+;; the screen persist after loading because of the action of
+;; display-buffer acting after the mode function during find-file.
+;; To approximate the best behaviour, we assume that this file is
+;; loaded by a call to proof-mode.  We display the screen now and add
+;; a wait procedure temporarily to proof-mode-hook which prevents
+;; redisplay until at least proof-internal-display-splash-time
+;; has elapsed. 
+
+;; Display the screen ASAP...
+(proof-display-splash-screen)
+
+(defun proof-wait-for-splash-proof-mode-hook-fn ()
+  "Wait for a while displaying splash screen, then remove self from hook." 
+  (if proof-display-splash
+       (let ((timer (get-itimer proof-welcome)))
+	 (if timer
+	     (if (< (- 40 proof-internal-display-splash-time)
+		    (itimer-value timer))
+		 ;; Splash has still not been seen for all of
+		 ;; internal-display-splash-time, set the timer
+		 ;; for the remaining time...
+		 (progn
+		   (set-itimer-value timer
+		    (- proof-internal-display-splash-time
+		       (- 40 (itimer-value timer))))
+		   ;; and wait until it finishes or user-input
+		   (while (and (get-itimer proof-welcome)
+			       (sit-for 1 t)))
+		   ;; If timer still running, run function
+		   ;; and delete timer.
+		   (if (itimer-live-p timer)
+		       (progn
+			 (funcall (itimer-function timer))
+			 (delete-itimer timer))))))))
+  (remove-hook 'proof-mode-hook 'proof-wait-for-splash-hook))
+
+(add-hook 'proof-mode-hook 'proof-wait-for-splash-proof-mode-hook-fn)
+
+
+(provide 'proof-splash)
+;; End of proof-splash.
diff --git a/generic/proof.el b/generic/proof.el
index 337e3a7a..e271cc99 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -1,4 +1,4 @@
-;; proof.el  Major mode for proof assistants
+;; proof.el  Proof General loader.
 ;;
 ;; Copyright (C) 1994 - 1998 LFCS Edinburgh. 
 ;; Authors: David Aspinall, Yves Bertot, Healfdene Goguen,
@@ -13,153 +13,12 @@
 ;; $Id$
 ;;
 
-(require 'proof-site)
+(require 'proof-site)			; site config
 
-(require 'proof-config)			
+(require 'proof-config)			; variables
 
-
-;;;
-;;; Splash screen (XEmacs specific for now)
-;;;
 (if (string-match "XEmacs" emacs-version)
-(progn     
-(require 'annotations)
-(defconst proof-welcome "*Proof General Welcome*"
-  "Name of the Proof General splash buffer.")
-
-(defconst proof-display-splash-image
-  ;; Use jpeg if we can, otherwise assume gif will work.
-  (if (featurep 'jpeg)
-      (cons 'jpeg
-	    (concat proof-internal-images-directory 
-		    "ProofGeneral.jpg"))
-  (cons 'gif
-	(concat proof-internal-images-directory 
-		(concat "ProofGeneral"
-			(or (and
-			     (fboundp 'device-pixel-depth)
-			     (> (device-pixel-depth) 8)
-			     ".gif")
-			    ;; Low colour gif for poor displays
-			    ".8bit.gif")))))
-  "Format and File name of Proof General Image.")
-
-(defcustom proof-display-splash 
-  (valid-instantiator-p
-   (vector (car proof-display-splash-image)
-		 :file (cdr proof-display-splash-image)) 'image)
-  "*Display splash screen when Proof General is loaded."
-  :type 'boolean
-  :group 'proof)
-
-(defcustom proof-internal-display-splash-time 4
-  "Minimum number of seconds to display splash screen for.
-If the machine gets to the end of proof-mode faster than this,
-we wait for the remaining time.  Must be a value less than 40."
-  :type 'integer
-  :group 'proof-internal)
-
-;; We take some care to preserve the users window configuration
-;; underneath the splash screen.  This is just to be polite.
-(defun proof-remove-splash-screen (conf)
-  "Make function to remove splash screen and restore window config to conf."
-  `(lambda ()
-     (and ;; If splash buffer is still alive 
-      (get-buffer proof-welcome)
-      (if (get-buffer-window (get-buffer proof-welcome))
-	  ;; Restore the window config if splash is being displayed
-	  (set-window-configuration ,conf)
-	t)
-      ;; And destroy splash buffer.
-      (kill-buffer proof-welcome))))
-
-(defun proof-display-splash-screen ()
-  "Save window config and display Proof General splash screen.
-No effect if proof-display-splash-time is zero."
-  (interactive)
-  (if proof-display-splash
-      (let*
-	  ((splashbuf   (get-buffer-create proof-welcome))
-	   (imglyph	(make-glyph
-			 (list (vector (car proof-display-splash-image) ':file
-				       (cdr proof-display-splash-image)))))
-	   ;; Keep win config explicitly instead of pushing/popping because
-	   ;; if the user switches windows by hand in some way, we want
-	   ;; to ignore the saved value.  Unfortunately there seems to
-	   ;; be no way currently to remove the top item of the stack.
-	   (removefn    (proof-remove-splash-screen
-			 (current-window-configuration))))
-	(save-excursion
-	  (set-buffer splashbuf)
-	  (erase-buffer)
-	  ;; FIXME: centre display better.  support FSFmacs.
-	  (insert "\n\n\n\t\t")
-	  (insert-char ?\  (/ (length proof-assistant) 2))
-	  (insert "    Welcome to\n\t\t  "
-		  proof-assistant " Proof General!\n\n\n\t\t ")
-	  (let ((ann (make-annotation imglyph))) ; reveal-annotation doesn't
-	    (reveal-annotation ann))	;      autoload, so use let form.  
-	  (insert "\n\n")
-	  (delete-other-windows (display-buffer splashbuf)))
-	;; Start the timer with a dummy value of 40 secs, to time the
-	;; loading of the rest of the mode.  This is a kludge to make
-	;; sure that the splash screen appears at least throughout the
-	;; load (which shouldn't last 40 secs!).  But if the load is
-	;; triggered by something other than a call to proof-mode,
-	;; the splash screen *will* appear for 40 secs (unless the
-	;; user kills it or switches buffer).
-	(redisplay-frame nil t)
-	(start-itimer proof-welcome removefn 40))))
-
-;; PROBLEM: when to call proof-display-splash-screen?  Effect we'd
-;; like is to call it during loading/initialising.  It's hard to make
-;; the screen persist after loading because of the action of
-;; display-buffer acting after the mode function during find-file.
-;; To approximate the best behaviour, we assume that this file is
-;; loaded by a call to proof-mode.  We display the screen now and add
-;; a wait procedure temporarily to proof-mode-hook which prevents
-;; redisplay until at least proof-internal-display-splash-time
-;; has elapsed. 
-
-;; Display the screen ASAP...
-(proof-display-splash-screen)
-
-(defun proof-wait-for-splash-proof-mode-hook-fn ()
-  "Wait for a while displaying splash screen, then remove self from hook." 
-  (if proof-display-splash
-       (let ((timer (get-itimer proof-welcome)))
-	 (if timer
-	     (if (< (- 40 proof-internal-display-splash-time)
-		    (itimer-value timer))
-		 ;; Splash has still not been seen for all of
-		 ;; internal-display-splash-time, set the timer
-		 ;; for the remaining time...
-		 (progn
-		   (set-itimer-value timer
-		    (- proof-internal-display-splash-time
-		       (- 40 (itimer-value timer))))
-		   ;; and wait until it finishes or user-input
-		   (while (and (get-itimer proof-welcome)
-			       (sit-for 1 t)))
-		   ;; If timer still running, run function
-		   ;; and delete timer.
-		   (if (itimer-live-p timer)
-		       (progn
-			 (funcall (itimer-function timer))
-			 (delete-itimer timer))))))))
-  (remove-hook 'proof-mode-hook 'proof-wait-for-splash-hook))
-
-(add-hook 'proof-mode-hook 'proof-wait-for-splash-proof-mode-hook-fn)
-
-))
-;;; End splash screen code
-
-
-
-;;;
-;;; Load included modules.
-;;;
-
+    (require 'proof-splash))			; splash screen
 
 ;; FIXME da: I think these ones should be autoloaded!!
 (require 'cl)
@@ -191,14 +50,12 @@ No effect if proof-display-splash-time is zero."
    (list 'make-variable-buffer-local (list 'quote var))
    (list 'setq-default var value)))
 
-;;
-;; Rest of code
-;;
 
 ;; Load toolbar code if toolbars available.
 (if (featurep 'toolbar)
     (require 'proof-toolbar))
 
+;; Main code is in these files
 (require 'proof-script)
 (require 'proof-shell)