Separated splash screen code

1 files changed, 140 insertions, 0 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.