1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
|
;; proof.el Major mode for proof assistants
;;
;; Copyright (C) 1994 - 1998 LFCS Edinburgh.
;; Authors: David Aspinall, Yves Bertot, Healfdene Goguen,
;; Thomas Kleymann and Dilip Sequeira
;;
;; Maintainer: Proof General maintainer <proofgen@dcs.ed.ac.uk>
;;
;; Thanks to Rod Burstall, Martin Hofmann,
;; James McKinna, Mark Ruys, Martin Steffen, Perdita Stevens
;; for helpful comments and code.
;;
;; $Id$
;;
(require 'proof-site)
(require 'proof-config)
;;;
;;; 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.
;;;
;; FIXME da: I think these ones should be autoloaded!!
(require 'cl)
(require 'compile)
(require 'comint)
(require 'etags)
(require 'easymenu)
;; Spans are our abstraction of extents/overlays.
(cond ((fboundp 'make-extent) (require 'span-extent))
((fboundp 'make-overlay) (require 'span-overlay))
(t nil))
(require 'proof-syntax)
(require 'proof-indent)
;; browse-url function doesn't seem to be autoloaded in
;; XEmacs 20.4, but it is in FSF Emacs 20.2.
(or (fboundp 'browse-url)
(autoload 'browse-url "browse-url"
"Ask a WWW browser to load URL." t))
(defmacro deflocal (var value &optional docstring)
"Define a buffer local variable VAR with default value VALUE."
(list 'progn
(list 'defvar var 'nil docstring)
(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))
(require 'proof-script)
(require 'proof-shell)
(provide 'proof)
;; proof.el ends here
|
