1 | ;; proof-utils.el Proof General utility functions |
---|
2 | ;; |
---|
3 | ;; Copyright (C) 1998-2002 LFCS Edinburgh. |
---|
4 | ;; Author: David Aspinall <David.Aspinall@ed.ac.uk> and others |
---|
5 | ;; License: GPL (GNU GENERAL PUBLIC LICENSE) |
---|
6 | ;; |
---|
7 | ;; proof-utils.el,v 8.13 2007/03/03 15:29:36 da Exp |
---|
8 | ;; |
---|
9 | ;; |
---|
10 | ;; Loading note: this file is required immediately from proof.el, so |
---|
11 | ;; no autoloads are used here. |
---|
12 | |
---|
13 | |
---|
14 | ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |
---|
15 | ;; |
---|
16 | ;; Handy macros |
---|
17 | |
---|
18 | (defmacro deflocal (var value &optional docstring) |
---|
19 | "Define a buffer local variable VAR with default value VALUE." |
---|
20 | `(progn |
---|
21 | (defvar ,var nil ,docstring) |
---|
22 | (make-variable-buffer-local (quote ,var)) |
---|
23 | (setq-default ,var ,value))) |
---|
24 | |
---|
25 | (defmacro proof-with-current-buffer-if-exists (buf &rest body) |
---|
26 | "As with-current-buffer if BUF exists and is live, otherwise nothing." |
---|
27 | `(if (buffer-live-p ,buf) |
---|
28 | (with-current-buffer ,buf |
---|
29 | ,@body))) |
---|
30 | |
---|
31 | ;; Slightly specialized version of above. This is used in commands |
---|
32 | ;; which work from different PG buffers (goals, response), typically |
---|
33 | ;; bound to toolbar commands. |
---|
34 | (defmacro proof-with-script-buffer (&rest body) |
---|
35 | "Execute BODY in some script buffer: current buf or otherwise proof-script-buffer. |
---|
36 | Return nil if not a script buffer or if no active scripting buffer." |
---|
37 | `(cond |
---|
38 | ((eq proof-buffer-type 'script) |
---|
39 | (progn |
---|
40 | ,@body)) |
---|
41 | ((buffer-live-p proof-script-buffer) |
---|
42 | (with-current-buffer proof-script-buffer |
---|
43 | ,@body)))) |
---|
44 | |
---|
45 | (defmacro proof-map-buffers (buflist &rest body) |
---|
46 | "Do BODY on each buffer in BUFLIST, if it exists." |
---|
47 | `(dolist (buf ,buflist) |
---|
48 | (proof-with-current-buffer-if-exists buf ,@body))) |
---|
49 | |
---|
50 | (defmacro proof-sym (string) |
---|
51 | "Return symbol for current proof assistant using STRING." |
---|
52 | `(intern (concat (symbol-name proof-assistant-symbol) "-" ,string))) |
---|
53 | |
---|
54 | |
---|
55 | (defun proof-try-require (symbol) |
---|
56 | "Try requiring SYMBOL. No error if the file for SYMBOL isn't found." |
---|
57 | (condition-case () |
---|
58 | (require symbol) |
---|
59 | (file-error nil)) |
---|
60 | (featurep symbol)) |
---|
61 | |
---|
62 | |
---|
63 | ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |
---|
64 | ;; |
---|
65 | ;; Simplified version of save-some-buffers, with useful arg |
---|
66 | ;; |
---|
67 | |
---|
68 | (defun proof-save-some-buffers (buffers) |
---|
69 | ;; code based on extract from files.el in XEmacs 21.4.14 |
---|
70 | (map-y-or-n-p |
---|
71 | (lambda (buffer) |
---|
72 | (if |
---|
73 | (and (buffer-modified-p buffer) |
---|
74 | (not (buffer-base-buffer buffer)) |
---|
75 | (buffer-file-name buffer)) |
---|
76 | ;; we deliberately don't switch to show the buffer; |
---|
77 | ;; let's assume user can see it or knows what's in it. |
---|
78 | (format "Save file %s? " |
---|
79 | (buffer-file-name buffer)))) |
---|
80 | (lambda (buffer) |
---|
81 | (set-buffer buffer) |
---|
82 | (condition-case () |
---|
83 | (save-buffer) |
---|
84 | (error nil))) |
---|
85 | buffers)) |
---|
86 | |
---|
87 | |
---|
88 | ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |
---|
89 | ;; |
---|
90 | ;; Function for taking action when dynamically adjusting customize values |
---|
91 | ;; |
---|
92 | (defun proof-set-value (sym value) |
---|
93 | "Set a customize variable using set-default and a function. |
---|
94 | We first call `set-default' to set SYM to VALUE. |
---|
95 | Then if there is a function SYM (i.e. with the same name as the |
---|
96 | variable SYM), it is called to take some dynamic action for the new |
---|
97 | setting. |
---|
98 | |
---|
99 | If there is no function SYM, we try stripping |
---|
100 | proof-assistant-symbol and adding \"proof-\" instead to get |
---|
101 | a function name. This extends proof-set-value to work with |
---|
102 | generic individual settings. |
---|
103 | |
---|
104 | The dynamic action call only happens when values *change*: as an |
---|
105 | approximation we test whether proof-config is fully-loaded yet." |
---|
106 | (set-default sym value) |
---|
107 | (if (featurep 'proof-config) |
---|
108 | (if (fboundp sym) |
---|
109 | (funcall sym) |
---|
110 | (if (> (length (symbol-name sym)) |
---|
111 | (+ 3 (length (symbol-name proof-assistant-symbol)))) |
---|
112 | (let ((generic |
---|
113 | (intern |
---|
114 | (concat "proof" |
---|
115 | (substring (symbol-name sym) |
---|
116 | (length (symbol-name |
---|
117 | proof-assistant-symbol))))))) |
---|
118 | (if (fboundp generic) |
---|
119 | (funcall generic))))))) |
---|
120 | |
---|
121 | |
---|
122 | |
---|
123 | ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |
---|
124 | ;; |
---|
125 | ;; Macros for defining per-assistant customization settings. |
---|
126 | ;; |
---|
127 | ;; This new mechanism is an improved way to handle per-assistant |
---|
128 | ;; settings. Instead of declaring a variable |
---|
129 | ;; "proof-assistant-web-page" and duplicating it in the prover |
---|
130 | ;; specific code to make the generic setting, we automatically declare |
---|
131 | ;; "isabelle-web-page", "coq-web-page", etc, using these macros. |
---|
132 | ;; |
---|
133 | ;; The advantage of this is that people's save settings will work |
---|
134 | ;; properly, and that it will become more possible to use more than |
---|
135 | ;; one instance of PG at a time. The disadvantage is that it is |
---|
136 | ;; slightly more complicated, and less "object-oriented" than the |
---|
137 | ;; previous approach. It is also a big change to move all settings. |
---|
138 | ;; |
---|
139 | ;; NB: this mechanism is work in progress in 3.2. It will |
---|
140 | ;; be expanded, although we may leave most low-level |
---|
141 | ;; settings to use the current mechanism. |
---|
142 | ;; |
---|
143 | ;; Notes: |
---|
144 | ;; |
---|
145 | ;; Two mechanisms for accessing generic vars: |
---|
146 | ;; |
---|
147 | ;; (proof-ass name) or (proof-assistant-name) |
---|
148 | ;; |
---|
149 | ;; Later is more efficient, though defining function |
---|
150 | ;; for each setting seems wasteful? |
---|
151 | |
---|
152 | (defun proof-ass-symv (sym) |
---|
153 | "Return the symbol for SYM for the current prover. SYM is evaluated." |
---|
154 | (intern (concat (symbol-name proof-assistant-symbol) "-" |
---|
155 | (symbol-name sym)))) |
---|
156 | |
---|
157 | (defmacro proof-ass-sym (sym) |
---|
158 | "Return the symbol for SYM for the current prover. SYM not evaluated." |
---|
159 | `(proof-ass-symv (quote ,sym))) |
---|
160 | |
---|
161 | (defun proof-defpgcustom-fn (sym args) |
---|
162 | "Define a new customization variable <PA>-sym for the current proof assistant. |
---|
163 | Helper for macro `defpgcustom'." |
---|
164 | (let ((specific-var (proof-ass-symv sym)) |
---|
165 | (generic-var (intern (concat "proof-assistant-" (symbol-name sym))))) |
---|
166 | (eval |
---|
167 | `(defcustom ,specific-var |
---|
168 | ,@args |
---|
169 | ;; FIXME: would be nicer to grab group from @args here and |
---|
170 | ;; prefix it automatically. For now, default to internals |
---|
171 | ;; setting for PA. |
---|
172 | ;; FIXME 2: would also be nice to grab docstring from args |
---|
173 | ;; and allow substitution for prover name, etc. A bit too |
---|
174 | ;; fancy perhaps! |
---|
175 | :group ,(quote proof-assistant-internals-cusgrp))) |
---|
176 | ;; For functions, we could simply use defalias. Unfortunately there |
---|
177 | ;; is nothing similar for values, so we define a new set/get function. |
---|
178 | (eval |
---|
179 | `(defun ,generic-var (&optional newval) |
---|
180 | ,(concat "Set or get value of " (symbol-name sym) " for current proof assistant. |
---|
181 | If NEWVAL is present, set the variable, otherwise return its current value.") |
---|
182 | (if newval |
---|
183 | (setq ,specific-var newval) |
---|
184 | ,specific-var))))) |
---|
185 | |
---|
186 | (defun undefpgcustom (sym) |
---|
187 | (let ((specific-var (proof-ass-symv sym)) |
---|
188 | (generic-var (intern (concat "proof-assistant-" (symbol-name sym))))) |
---|
189 | (pg-custom-undeclare-variable specific-var) |
---|
190 | (fmakunbound generic-var))) |
---|
191 | |
---|
192 | (defmacro defpgcustom (sym &rest args) |
---|
193 | "Define a new customization variable <PA>-SYM for the current proof assistant. |
---|
194 | The function proof-assistant-<SYM> is also defined, which can be used in the |
---|
195 | generic portion of Proof General to set and retrieve the value for the current p.a. |
---|
196 | Arguments as for `defcustom', which see. |
---|
197 | |
---|
198 | Usage: (defpgcustom SYM &rest ARGS)." |
---|
199 | `(proof-defpgcustom-fn (quote ,sym) (quote ,args))) |
---|
200 | |
---|
201 | (defmacro proof-ass (sym) |
---|
202 | "Return the value for SYM for the current prover." |
---|
203 | ;; (eval `(proof-ass-sym ,sym)) |
---|
204 | `(symbol-value (proof-ass-symv ',sym))) ;; [Stefan Monnier] |
---|
205 | |
---|
206 | (defun proof-defpgdefault-fn (sym value) |
---|
207 | "Helper for `defpgdefault', which see. SYM and VALUE are evaluated." |
---|
208 | ;; NB: we need this because nothing in customize library seems to do |
---|
209 | ;; the right thing. |
---|
210 | (let ((symbol (proof-ass-symv sym))) |
---|
211 | (set-default symbol |
---|
212 | (cond |
---|
213 | ;; Use saved value if it's set |
---|
214 | ((get symbol 'saved-value) |
---|
215 | (car (get symbol 'saved-value))) |
---|
216 | ;; Otherwise override old default with new one |
---|
217 | (t |
---|
218 | value))))) |
---|
219 | |
---|
220 | (defmacro defpgdefault (sym value) |
---|
221 | "Set default for the proof assistant specific variable <PA>-SYM to VALUE. |
---|
222 | This should be used in prover-specific code to alter the default values |
---|
223 | for prover specific settings. |
---|
224 | |
---|
225 | Usage: (defpgdefault SYM VALUE)" |
---|
226 | `(proof-defpgdefault-fn (quote ,sym) ,value)) |
---|
227 | |
---|
228 | ;; |
---|
229 | ;; Make a function named for the current proof assistant. |
---|
230 | ;; |
---|
231 | (defmacro defpgfun (name arglist &rest args) |
---|
232 | "Define function <PA>-SYM as for defun." |
---|
233 | `(defun ,(proof-ass-symv name) ,arglist |
---|
234 | ,@args)) |
---|
235 | |
---|
236 | |
---|
237 | ;; |
---|
238 | ;; End macros |
---|
239 | ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |
---|
240 | |
---|
241 | |
---|
242 | ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |
---|
243 | ;; |
---|
244 | ;; Buffers and filenames |
---|
245 | |
---|
246 | (defun proof-file-truename (filename) |
---|
247 | "Returns the true name of the file FILENAME or nil if file non-existent." |
---|
248 | (and filename (file-exists-p filename) (file-truename filename))) |
---|
249 | |
---|
250 | (defun proof-file-to-buffer (filename) |
---|
251 | "Find a buffer visiting file FILENAME, or nil if there isn't one." |
---|
252 | (let* ((buffers (buffer-list)) |
---|
253 | (pos |
---|
254 | (position (file-truename filename) |
---|
255 | (mapcar 'proof-file-truename |
---|
256 | (mapcar 'buffer-file-name |
---|
257 | buffers)) |
---|
258 | :test 'equal))) |
---|
259 | (and pos (nth pos buffers)))) |
---|
260 | |
---|
261 | (defun proof-files-to-buffers (filenames) |
---|
262 | "Converts a list of FILENAMES into a list of BUFFERS." |
---|
263 | (if (null filenames) nil |
---|
264 | (let* ((buffer (proof-file-to-buffer (car filenames))) |
---|
265 | (rest (proof-files-to-buffers (cdr filenames)))) |
---|
266 | (if buffer (cons buffer rest) rest)))) |
---|
267 | |
---|
268 | (defun proof-buffers-in-mode (mode &optional buflist) |
---|
269 | "Return a list of the buffers in the buffer list in major-mode MODE. |
---|
270 | Restrict to BUFLIST if it's set." |
---|
271 | (let ((bufs-left (or buflist (buffer-list))) |
---|
272 | bufs-got) |
---|
273 | (dolist (buf bufs-left bufs-got) |
---|
274 | (if (with-current-buffer buf (eq mode major-mode)) |
---|
275 | (setq bufs-got (cons buf bufs-got)))))) |
---|
276 | |
---|
277 | ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |
---|
278 | ;; |
---|
279 | ;; Associated buffers |
---|
280 | ;; |
---|
281 | |
---|
282 | (defun pg-save-from-death () |
---|
283 | "Prevent this associated buffer from being killed: merely erase it. |
---|
284 | A hook function for `kill-buffer-hook'. |
---|
285 | This is a fairly crude and not-entirely-robust way to prevent the |
---|
286 | user accidently killing an associated buffer." |
---|
287 | (if (and (proof-shell-live-buffer) proof-buffer-type) |
---|
288 | (progn |
---|
289 | (let ((bufname (buffer-name))) |
---|
290 | (bufhist-erase-buffer) |
---|
291 | (set-buffer-modified-p nil) |
---|
292 | (bury-buffer) |
---|
293 | (error |
---|
294 | "Warning: buffer %s not killed; still associated with prover process." |
---|
295 | bufname))))) |
---|
296 | |
---|
297 | ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |
---|
298 | ;; |
---|
299 | ;; Key functions |
---|
300 | |
---|
301 | (defun proof-define-keys (map kbl) |
---|
302 | "Adds keybindings KBL in MAP. |
---|
303 | The argument KBL is a list of tuples (k . f) where `k' is a keybinding |
---|
304 | \(vector) and `f' the designated function." |
---|
305 | (mapcar |
---|
306 | (lambda (kbl) |
---|
307 | (let ((k (car kbl)) (f (cdr kbl))) |
---|
308 | (define-key map k f))) |
---|
309 | kbl)) |
---|
310 | |
---|
311 | ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |
---|
312 | ;; |
---|
313 | ;; Managing font-lock |
---|
314 | ;; |
---|
315 | |
---|
316 | ;; Notes: |
---|
317 | ;; |
---|
318 | ;; * Various mechanisms for setting defaults, different between |
---|
319 | ;; Emacsen. Old method(?) was to set "blah-mode-font-lock-keywords" |
---|
320 | ;; and copy it into "font-lock-keywords" to engage font-lock. |
---|
321 | ;; Present method for XEmacs is to put a 'font-lock-defaults |
---|
322 | ;; property on the major-mode symbol, or use font-lock-defaults |
---|
323 | ;; buffer local variable. We use the latter. |
---|
324 | ;; |
---|
325 | ;; * Buffers which are output-only are *not* kept in special minor |
---|
326 | ;; modes font-lock-mode (or x-symbol-mode). In case the user |
---|
327 | ;; doesn't want fontification we have a user option, |
---|
328 | ;; proof-output-fontify-enable. |
---|
329 | |
---|
330 | (deflocal proof-font-lock-keywords nil |
---|
331 | "Value of font-lock-keywords in this buffer. |
---|
332 | We set `font-lock-defaults' to '(proof-font-lock-keywords t) for |
---|
333 | compatibility with X-Symbol, which may hack `proof-font-lock-keywords' |
---|
334 | with extra patterns (in non-mule mode).") |
---|
335 | |
---|
336 | (deflocal proof-font-lock-keywords-case-fold-search nil |
---|
337 | "Value of font-lock-keywords-case-fold-search in this buffer.") |
---|
338 | |
---|
339 | (defun proof-font-lock-configure-defaults (autofontify &optional case-fold) |
---|
340 | "Set defaults for font-lock based on current font-lock-keywords. |
---|
341 | This is a delicate operation, because we only want to use font-lock-mode |
---|
342 | in some buffers, so we have to tread carefully around the font-lock |
---|
343 | code to avoid it turning itself on in the buffers where that actually |
---|
344 | *breaks* fontification. |
---|
345 | |
---|
346 | AUTOFONTIFY must be nil for buffers where we may want to really use |
---|
347 | font-lock-mode." |
---|
348 | ;; |
---|
349 | ;; At the moment, the specific assistant code hacks |
---|
350 | ;; font-lock-keywords. Here we use that value to hack |
---|
351 | ;; font-lock-defaults, which is used by font-lock to set |
---|
352 | ;; font-lock-keywords from again!! Yuk. |
---|
353 | ;; |
---|
354 | ;; Previously, 'font-lock-keywords was used directly as a setting |
---|
355 | ;; for the defaults. This has a bad interaction with x-symbol which |
---|
356 | ;; edits font-lock-keywords and loses the setting. So we make a |
---|
357 | ;; copy of it in a new local variable, proof-font-lock-keywords. |
---|
358 | ;; |
---|
359 | (make-local-variable 'proof-font-lock-keywords) |
---|
360 | (make-local-variable 'proof-font-lock-keywords-case-fold-search) |
---|
361 | (setq proof-font-lock-keywords font-lock-keywords) |
---|
362 | (setq proof-font-lock-keywords-case-fold-search case-fold) |
---|
363 | ;; Setting font-lock-defaults explicitly is required by FSF Emacs |
---|
364 | ;; 20.4's version of font-lock in any case. |
---|
365 | |
---|
366 | (if autofontify |
---|
367 | (progn |
---|
368 | (make-local-variable 'font-lock-defaults) ; needed?? |
---|
369 | (setq font-lock-defaults `(proof-font-lock-keywords nil ,case-fold)) |
---|
370 | ;; 12.1.99: For XEmacs, we must also set the mode property. |
---|
371 | ;; This is needed for buffers which are put into font-lock-mode |
---|
372 | ;; (rather than fontified by hand). |
---|
373 | (put major-mode 'font-lock-defaults font-lock-defaults)) |
---|
374 | ;; 11.12.01: Emacs 21 is very eager about turning on font |
---|
375 | ;; lock and has hooks all over the place to do it. To make |
---|
376 | ;; sure it doesn't happen we have to eradicate all sense of |
---|
377 | ;; having any fontification ability. |
---|
378 | (proof-font-lock-clear-font-lock-vars) |
---|
379 | ;; In fact, this still leaves font-lock switched on! But |
---|
380 | ;; hopefully in a useless way. XEmacs has better control |
---|
381 | ;; over which modes not to enable it for (although annoying |
---|
382 | ;; that it's a custom setting) |
---|
383 | (if proof-running-on-XEmacs |
---|
384 | (setq font-lock-mode-disable-list |
---|
385 | (cons major-mode font-lock-mode-disable-list))))) |
---|
386 | |
---|
387 | (defun proof-font-lock-clear-font-lock-vars () |
---|
388 | (kill-local-variable 'font-lock-defaults) |
---|
389 | (kill-local-variable 'font-lock-keywords) |
---|
390 | (setq font-lock-keywords nil) |
---|
391 | (put major-mode 'font-lock-defaults nil) |
---|
392 | ;; Ensure it's switched off, too. |
---|
393 | ;; NB: this tends to undo the hard work we've done |
---|
394 | ;; by unfontifying, so don't do that now |
---|
395 | ;; (font-lock-mode -1)) |
---|
396 | ) |
---|
397 | |
---|
398 | (defun proof-font-lock-set-font-lock-vars () |
---|
399 | (setq font-lock-defaults |
---|
400 | `(proof-font-lock-keywords |
---|
401 | nil |
---|
402 | ,proof-font-lock-keywords-case-fold-search)) |
---|
403 | (setq font-lock-keywords proof-font-lock-keywords)) |
---|
404 | |
---|
405 | (defun proof-fontify-region (start end &optional keepspecials) |
---|
406 | "Fontify and decode X-Symbols in region START...END. |
---|
407 | Fontifies according to the buffer's font lock defaults. |
---|
408 | Uses `proof-x-symbol-decode-region' to decode tokens |
---|
409 | if X-Symbol is enabled. |
---|
410 | |
---|
411 | If `pg-use-specials-for-fontify' is set, remove characters |
---|
412 | with top bit set after fontifying so they don't spoil cut and paste, |
---|
413 | unless KEEPSPECIALS is set to override this. |
---|
414 | |
---|
415 | Returns new END value." |
---|
416 | ;; We fontify first because X-sym decoding changes char positions. |
---|
417 | ;; It's okay because x-symbol-decode works even without font lock. |
---|
418 | ;; Possible disadvantage is that font lock patterns can't refer |
---|
419 | ;; to X-Symbol characters. |
---|
420 | ;; NB: perhaps we can narrow within the whole function, but there |
---|
421 | ;; was an earlier problem with doing that. |
---|
422 | (if proof-output-fontify-enable |
---|
423 | (progn |
---|
424 | ;; Temporarily set font-lock defaults |
---|
425 | (proof-font-lock-set-font-lock-vars) |
---|
426 | |
---|
427 | ;; Yukky hacks to immorally interface with font-lock |
---|
428 | (unless proof-running-on-XEmacs |
---|
429 | (font-lock-set-defaults)) |
---|
430 | (let ((font-lock-keywords proof-font-lock-keywords)) |
---|
431 | (if (and proof-running-on-XEmacs |
---|
432 | (>= emacs-major-version 21) |
---|
433 | (>= emacs-minor-version 4) |
---|
434 | (not font-lock-cache-position)) |
---|
435 | (progn |
---|
436 | (setq font-lock-cache-position (make-marker)) |
---|
437 | (set-marker font-lock-cache-position 0))) |
---|
438 | |
---|
439 | (save-restriction |
---|
440 | (narrow-to-region start end) |
---|
441 | (run-hooks 'pg-before-fontify-output-hook) |
---|
442 | (setq end (point-max))) |
---|
443 | ;; da: 10.8.04 protect this against "Nesting too deep for parser" |
---|
444 | ;; which may be raised by XEmacs' crummy `parse-partial-sexp'. |
---|
445 | (condition-case err |
---|
446 | (font-lock-default-fontify-region start end nil) |
---|
447 | (t (proof-debug "Caught condition %s in `font-lock-default-fontify-region'" |
---|
448 | (car err))))))) |
---|
449 | (save-restriction |
---|
450 | (narrow-to-region start end) |
---|
451 | (run-hooks 'pg-after-fontify-output-hook) |
---|
452 | (setq end (point-max))) |
---|
453 | (if (and pg-use-specials-for-fontify (not keepspecials)) |
---|
454 | (progn |
---|
455 | (pg-remove-specials start end) |
---|
456 | (setq end (point)))) |
---|
457 | (prog1 |
---|
458 | ;; prog1 because we return new END value. |
---|
459 | (if (proof-ass x-symbol-enable) |
---|
460 | (proof-x-symbol-decode-region start end)) |
---|
461 | (proof-font-lock-clear-font-lock-vars))) |
---|
462 | |
---|
463 | (defun pg-remove-specials (&optional start end) |
---|
464 | "Remove special characters in region. Default to whole buffer. |
---|
465 | Leave point at END." |
---|
466 | (save-restriction |
---|
467 | (if (and start end) |
---|
468 | (narrow-to-region start end)) |
---|
469 | (goto-char (or start (point-min))) |
---|
470 | (replace-regexp pg-special-char-regexp "") |
---|
471 | (goto-char (point-max)))) |
---|
472 | |
---|
473 | (defun pg-remove-specials-in-string (string) |
---|
474 | (proof-replace-regexp-in-string pg-special-char-regexp "" string)) |
---|
475 | |
---|
476 | |
---|
477 | |
---|
478 | ;; FIXME todo: add toggle for fontify region which turns it on/off |
---|
479 | |
---|
480 | (defun proof-fontify-buffer () |
---|
481 | "Call proof-fontify-region on whole buffer." |
---|
482 | (proof-fontify-region (point-min) (point-max))) |
---|
483 | |
---|
484 | |
---|
485 | |
---|
486 | |
---|
487 | ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |
---|
488 | ;; |
---|
489 | ;; Messaging and display functions |
---|
490 | ;; |
---|
491 | |
---|
492 | |
---|
493 | (defun proof-warn-if-unset (tag sym) |
---|
494 | "Give a warning (with TAG) if symbol SYM is unbound or nil." |
---|
495 | (unless (and (boundp sym) (symbol-value sym)) |
---|
496 | (warn "Proof General %s: %s is unset." tag (symbol-name sym)))) |
---|
497 | |
---|
498 | (defun proof-get-window-for-buffer (buffer) |
---|
499 | "Find a window for BUFFER, display it there, return the window. |
---|
500 | NB: may change the selected window." |
---|
501 | ;; IF there *isn't* a visible window showing buffer... |
---|
502 | (unless (get-buffer-window buffer 0) |
---|
503 | ;; THEN find somewhere nice to display it |
---|
504 | (if (and |
---|
505 | ;; If we're in two-window mode and already displaying a |
---|
506 | ;; script/response/goals, try to just switch the buffer |
---|
507 | ;; instead of calling display-buffer which alters sizes. |
---|
508 | ;; Gives user some stability on display. |
---|
509 | (not proof-three-window-enable) |
---|
510 | (> (count-windows) 1) |
---|
511 | ;; was: (not (eq (next-window) (selected-window))) |
---|
512 | (memq (window-buffer (next-window nil 'ignoreminibuf)) |
---|
513 | ;; NB: 3.5: added rest of assoc'd buffers here |
---|
514 | (cons proof-script-buffer (proof-associated-buffers)))) |
---|
515 | (if (eq (selected-window) (minibuffer-window)) |
---|
516 | ;; 17.8.01: avoid switching the minibuffer's contents |
---|
517 | ;; -- terrrible confusion -- use next-window after |
---|
518 | ;; script buffer instead. |
---|
519 | ;; (another hack which is mostly right) |
---|
520 | (set-window-buffer |
---|
521 | (next-window |
---|
522 | (car-safe (get-buffer-window-list proof-script-buffer)) |
---|
523 | 'ignoreminibuf) buffer) |
---|
524 | (if (eq (window-buffer (next-window nil 'ignoreminibuf)) |
---|
525 | proof-script-buffer) |
---|
526 | ;; switch this window |
---|
527 | (set-window-buffer (selected-window) buffer) |
---|
528 | ;; switch other window |
---|
529 | (set-window-buffer (next-window nil 'ignoreminibuf) buffer))) |
---|
530 | ;; o/w: call display buffer to configure windows nicely. |
---|
531 | (display-buffer buffer))) |
---|
532 | ;; Return the window, hopefully the one we first thought of. |
---|
533 | (get-buffer-window buffer 0)) |
---|
534 | |
---|
535 | (defun proof-display-and-keep-buffer (buffer &optional pos) |
---|
536 | "Display BUFFER and make window according to display mode. |
---|
537 | If optional POS is present, will set point to POS. |
---|
538 | If POS is a string, search for this string. |
---|
539 | Otherwise move point to the end of the buffer. |
---|
540 | Ensure that point is visible in window." |
---|
541 | (save-excursion |
---|
542 | (save-selected-window |
---|
543 | (let ((window (proof-get-window-for-buffer buffer))) |
---|
544 | (if (window-live-p window) ;; [fails sometimes?] |
---|
545 | (progn |
---|
546 | ;; Set the size and point position. |
---|
547 | (if proof-three-window-enable |
---|
548 | (set-window-dedicated-p window proof-three-window-enable)) |
---|
549 | (select-window window) |
---|
550 | (if proof-shrink-windows-tofit |
---|
551 | (proof-resize-window-tofit) |
---|
552 | ;; If we're not shrinking to fit, allow the size of |
---|
553 | ;; this window to change. [NB: might be nicer to |
---|
554 | ;; fix the size based on user choice] |
---|
555 | (setq window-size-fixed nil)) |
---|
556 | ;; For various reasons, point may get moved around in |
---|
557 | ;; response buffer. Attempt to normalise its position. |
---|
558 | (if (stringp pos) |
---|
559 | (progn (goto-char (point-min)) |
---|
560 | (search-forward pos nil t) |
---|
561 | (recenter)) |
---|
562 | (goto-char (or pos (point-max)))) |
---|
563 | (if pos |
---|
564 | (beginning-of-line) |
---|
565 | (skip-chars-backward "\n\t ")) |
---|
566 | ;; Ensure point visible. Again, window may have died |
---|
567 | ;; inside shrink to fit, for some reason |
---|
568 | (if (window-live-p window) |
---|
569 | (unless (pos-visible-in-window-p (point) window) |
---|
570 | (recenter -1))))))))) |
---|
571 | |
---|
572 | (defun proof-clean-buffer (buffer) |
---|
573 | "Erase buffer and hide from display if proof-delete-empty-windows set. |
---|
574 | Auto deletion only affects selected frame. (We assume that the selected |
---|
575 | frame is the one showing the script buffer.) |
---|
576 | No effect if buffer is dead." |
---|
577 | (if (buffer-live-p buffer) |
---|
578 | (with-current-buffer buffer |
---|
579 | (unless (eq 0 (buffer-size)) ;; checkpoint unless already empty |
---|
580 | (bufhist-checkpoint-and-erase)) |
---|
581 | (set-buffer-modified-p nil) |
---|
582 | (if (eq buffer proof-response-buffer) |
---|
583 | (setq pg-response-next-error nil)) ; all error msgs lost! |
---|
584 | (if proof-delete-empty-windows |
---|
585 | (delete-windows-on buffer t))))) |
---|
586 | |
---|
587 | (defun proof-message (&rest args) |
---|
588 | "Issue the message ARGS in the response buffer and display it." |
---|
589 | (pg-response-display-with-face (apply 'concat args)) |
---|
590 | (proof-display-and-keep-buffer proof-response-buffer)) |
---|
591 | |
---|
592 | (defun proof-warning (&rest args) |
---|
593 | "Issue the warning ARGS in the response buffer and display it. |
---|
594 | The warning is coloured with proof-warning-face." |
---|
595 | (pg-response-display-with-face (apply 'concat args) 'proof-warning-face) |
---|
596 | (proof-display-and-keep-buffer proof-response-buffer)) |
---|
597 | |
---|
598 | (defun pg-internal-warning (message &rest args) |
---|
599 | "Display internal warning MESSAGE with ARGS as for format." |
---|
600 | (let ((formatted (apply 'format message args))) |
---|
601 | (if (fboundp 'display-warning) |
---|
602 | (display-warning 'proof-general formatted) |
---|
603 | (message formatted)))) |
---|
604 | |
---|
605 | ;; could be a macro for efficiency in compiled code |
---|
606 | (defun proof-debug (msg &rest args) |
---|
607 | "Issue the debugging message (format MSG ARGS) in the response buffer, display it. |
---|
608 | If proof-show-debug-messages is nil, do nothing." |
---|
609 | (if proof-show-debug-messages |
---|
610 | (let ((formatted (apply 'format msg args))) |
---|
611 | (if (fboundp 'display-warning) ;; use builtin warning system in XEmacs |
---|
612 | (display-warning 'proof-general formatted 'info) |
---|
613 | ;; otherwise use response buffer with dedicated font, & display it |
---|
614 | (progn |
---|
615 | (pg-response-display-with-face formatted 'proof-debug-message-face) |
---|
616 | (proof-display-and-keep-buffer proof-response-buffer)))))) |
---|
617 | |
---|
618 | |
---|
619 | ;;; A handy utility function used in the "Buffers" menu, and throughout |
---|
620 | ;; the code. |
---|
621 | (defun proof-switch-to-buffer (buf &optional noselect) |
---|
622 | "Switch to or display buffer BUF in other window unless already displayed. |
---|
623 | If optional arg NOSELECT is true, don't switch, only display it. |
---|
624 | No action if BUF is nil or killed." |
---|
625 | ;; Maybe this needs to be more sophisticated, using |
---|
626 | ;; proof-display-and-keep-buffer ? |
---|
627 | (and (buffer-live-p buf) |
---|
628 | (unless (eq buf (window-buffer (selected-window))) |
---|
629 | (if noselect |
---|
630 | ;; FIXME: would like 'norecord arg here to override |
---|
631 | ;; previous window entering top of MRU list here. |
---|
632 | ;; In fact, this could be hacked in XEmacs code. |
---|
633 | ;; GNU Emacs seems *not* to put previously displayed |
---|
634 | ;; window onto the top of the list with record-buffer: |
---|
635 | ;; that gives much nicer behaviour than XEmacs here. |
---|
636 | (display-buffer buf 'not-this-window) |
---|
637 | (let ((pop-up-windows t)) |
---|
638 | (pg-pop-to-buffer buf 'not-this-window 'norecord)))))) |
---|
639 | |
---|
640 | |
---|
641 | ;; Originally based on `shrink-window-if-larger-than-buffer', which |
---|
642 | ;; has a pretty wierd implementation. |
---|
643 | ;; TODO: desirable improvements would be to add some crafty history based |
---|
644 | ;; on user resize-events. E.g. user resizes window, that becomes the |
---|
645 | ;; new maximum size. |
---|
646 | ;; FIXME: GNU Emacs has useful "window-size-fixed" which we use |
---|
647 | ;; HOWEVER, it's still not quite the right thing, it seems to me. |
---|
648 | ;; We'd like to specifiy a *minimum size* for a given buffer, |
---|
649 | ;; not a maximum. With a frame split with just goals/response |
---|
650 | ;; we'd still get resize errors here using window-size-fixed. |
---|
651 | ;; FIXME: shrink-to-fit doesn't really work in three-buffer mode, |
---|
652 | ;; since shrinking one of the associated buffers tends to enlarge the |
---|
653 | ;; other (rather than just enlarging the proof state) |
---|
654 | (defun proof-resize-window-tofit (&optional window) |
---|
655 | "Shrink the WINDOW to be as small as possible to display its contents. |
---|
656 | Do not shrink to less than `window-min-height' lines. |
---|
657 | Do nothing if the buffer contains more lines than the present window height, |
---|
658 | or if some of the window's contents are scrolled out of view, |
---|
659 | or if the window is not the full width of the frame, |
---|
660 | or if the window is the only window of its frame." |
---|
661 | ;; da: actually seems okay in this case |
---|
662 | (interactive) |
---|
663 | (or window (setq window (selected-window))) |
---|
664 | ;; some checks before resizing to avoid messing custom display |
---|
665 | ;; [probably somewhat superfluous/extra rare] |
---|
666 | (if |
---|
667 | (or |
---|
668 | ;; The frame must not be minibuffer-only. |
---|
669 | (eq (frame-parameter (window-frame window) 'minibuffer) 'only) |
---|
670 | ;; We've got more than one window, right? |
---|
671 | (= 1 (let ((frame (selected-frame))) |
---|
672 | (select-frame (window-frame window)) |
---|
673 | (unwind-protect ;; [why is this protected?] |
---|
674 | (count-windows) |
---|
675 | (select-frame frame) |
---|
676 | (select-window window)))) |
---|
677 | ;; the window is the full width, right? |
---|
678 | ;; [if not, we may be in horiz-split scheme, problematic] |
---|
679 | (not (window-leftmost-p window)) |
---|
680 | (not (window-rightmost-p window))) |
---|
681 | ;; OK, we're not going to adjust the height here. Moreover, |
---|
682 | ;; we'll make sure the height can be changed elsewhere. |
---|
683 | (setq window-size-fixed nil) |
---|
684 | (with-current-buffer (window-buffer window) |
---|
685 | (let* |
---|
686 | ;; weird test cases: |
---|
687 | ;; cur=45, max=23, desired=121, extraline=0 |
---|
688 | ;; current height |
---|
689 | ;;; ((cur-height (window-height window)) |
---|
690 | ;; Most window is allowed to grow to |
---|
691 | ((max-height |
---|
692 | (/ (frame-height (window-frame window)) |
---|
693 | (if proof-three-window-enable |
---|
694 | ;; we're in three-window-mode with |
---|
695 | ;; all horizontal splits, so share the height. |
---|
696 | 3 |
---|
697 | ;; Otherwise assume a half-and-half split |
---|
698 | 2))) |
---|
699 | ;; If buffer ends with a newline, ignore it when counting |
---|
700 | ;; height unless point is after it. |
---|
701 | (extraline |
---|
702 | (if (and (not (eobp)) |
---|
703 | (eq ?\n (char-after (1- (point-max))))) |
---|
704 | 1 0)) |
---|
705 | (test-pos (- (point-max) extraline)) |
---|
706 | ;; Direction of resizing based on whether max position is |
---|
707 | ;; currently visible. [ FIXME: not completely sensible: |
---|
708 | ;; may be displaying end fraction of buffer! ] |
---|
709 | ;; (shrink (pos-visible-in-window-p test-pos window)) |
---|
710 | ;; Likely desirable height is given by count-lines |
---|
711 | (desired-height |
---|
712 | ;; FIXME: is count-lines too expensive for v.large |
---|
713 | ;; buffers? Probably not an issue for us, but one |
---|
714 | ;; wonders at the shrink to fit strategy. |
---|
715 | ;; NB: way to calculate pixel fraction? |
---|
716 | (+ extraline 1 (count-lines (point-min) (point-max))))) |
---|
717 | ;; Let's shrink or expand. Uses new GNU Emacs function. |
---|
718 | (let ((window-size-fixed nil)) |
---|
719 | (set-window-text-height window desired-height)) |
---|
720 | ;; (cond |
---|
721 | ;; ((and shrink |
---|
722 | ;; (> cur-height window-min-height) |
---|
723 | ;; ;; don't shrink if already too big; leave where it is |
---|
724 | ;; (< cur-height max-height)) |
---|
725 | ;; (with-selected-window |
---|
726 | ;; window |
---|
727 | ;; (shrink-window (- cur-height (max window-min-height desired-height))))) |
---|
728 | ;; (;; expand |
---|
729 | ;; (< cur-height max-height) |
---|
730 | ;; (with-selected-window window |
---|
731 | ;; (enlarge-window |
---|
732 | ;; (- (min max-height desired-height) cur-height))))) |
---|
733 | ;; If we're at least the desirable height, it must be that the |
---|
734 | ;; whole buffer can be seen --- so make sure display starts at |
---|
735 | ;; beginning. |
---|
736 | ;; NB: shrinking windows can sometimes delete them |
---|
737 | ;; (although we don't want it to here!), but make this next |
---|
738 | ;; check for robustness. |
---|
739 | (if (window-live-p window) |
---|
740 | (progn |
---|
741 | (if (>= (window-height window) desired-height) |
---|
742 | (set-window-start window (point-min))) |
---|
743 | ;; window-size-fixed is a GNU Emacs buffer local variable |
---|
744 | ;; which determines window size of buffer. |
---|
745 | ;; (setq window-size-fixed (window-height window)) |
---|
746 | )))))) |
---|
747 | |
---|
748 | |
---|
749 | ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |
---|
750 | ;; |
---|
751 | ;; Function for submitting bug reports. |
---|
752 | ;; |
---|
753 | |
---|
754 | (defun proof-submit-bug-report () |
---|
755 | "Submit an bug report or other report for Proof General." |
---|
756 | (interactive) |
---|
757 | (require 'reporter) |
---|
758 | (let |
---|
759 | ((reporter-prompt-for-summary-p |
---|
760 | "(Very) brief summary of problem or suggestion: ")) |
---|
761 | (reporter-submit-bug-report |
---|
762 | "da+pg-bugs@inf.ed.ac.uk" |
---|
763 | "Proof General" |
---|
764 | (list 'proof-general-version 'proof-assistant |
---|
765 | 'x-symbol-version) |
---|
766 | nil nil |
---|
767 | "[ When reporting a bug, please include a small test case for us to repeat it. |
---|
768 | Please also check that it is not already covered in the BUGS or FAQ files that came with |
---|
769 | the distribution, or the latest versions at |
---|
770 | http://proofgeneral.inf.ed.ac.uk/ProofGeneral/BUGS and |
---|
771 | http://proofgeneral.inf.ed.ac.uk/ProofGeneral/FAQ ]"))) |
---|
772 | |
---|
773 | |
---|
774 | ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |
---|
775 | ;;; |
---|
776 | ;;; Utils for making functions to adjust user settings |
---|
777 | ;;; |
---|
778 | |
---|
779 | (defun proof-deftoggle-fn (var &optional othername) |
---|
780 | "Define a function <VAR>-toggle for toggling a boolean customize setting VAR. |
---|
781 | Args as for the macro `proof-deftoggle', except will be evaluated." |
---|
782 | (eval |
---|
783 | `(defun ,(if othername othername |
---|
784 | (intern (concat (symbol-name var) "-toggle"))) (arg) |
---|
785 | ,(concat "Toggle `" (symbol-name var) "'. With ARG, turn on iff ARG>0. |
---|
786 | This function simply uses customize-set-variable to set the variable. |
---|
787 | It was constructed with `proof-deftoggle-fn'.") |
---|
788 | (interactive "P") |
---|
789 | (customize-set-variable |
---|
790 | (quote ,var) |
---|
791 | (if (null arg) (not ,var) |
---|
792 | (> (prefix-numeric-value arg) 0)))))) |
---|
793 | |
---|
794 | (defmacro proof-deftoggle (var &optional othername) |
---|
795 | "Define a function VAR-toggle for toggling a boolean customize setting VAR. |
---|
796 | The toggle function uses customize-set-variable to change the variable. |
---|
797 | OTHERNAME gives an alternative name than the default <VAR>-toggle. |
---|
798 | The name of the defined function is returned." |
---|
799 | `(proof-deftoggle-fn (quote ,var) (quote ,othername))) |
---|
800 | |
---|
801 | (defun proof-defintset-fn (var &optional othername) |
---|
802 | "Define a function <VAR>-intset for setting an integer customize setting VAR. |
---|
803 | Args as for the macro `proof-defintset', except will be evaluated." |
---|
804 | (eval |
---|
805 | `(defun ,(if othername othername |
---|
806 | (intern (concat (symbol-name var) "-intset"))) (arg) |
---|
807 | ,(concat "Set `" (symbol-name var) "' to ARG. |
---|
808 | This function simply uses customize-set-variable to set the variable. |
---|
809 | It was constructed with `proof-defintset-fn'.") |
---|
810 | (interactive ,(format "nValue for %s (int, currently %s):" |
---|
811 | (symbol-name var) |
---|
812 | (symbol-value var))) |
---|
813 | (customize-set-variable (quote ,var) arg)))) |
---|
814 | |
---|
815 | (defmacro proof-defintset (var &optional othername) |
---|
816 | "Define a function <VAR>-intset for setting an integer customize setting VAR. |
---|
817 | The setting function uses customize-set-variable to change the variable. |
---|
818 | OTHERNAME gives an alternative name than the default <VAR>-intset. |
---|
819 | The name of the defined function is returned." |
---|
820 | `(proof-defintset-fn (quote ,var) (quote ,othername))) |
---|
821 | |
---|
822 | (defun proof-defstringset-fn (var &optional othername) |
---|
823 | "Define a function <VAR>-toggle for setting an integer customize setting VAR. |
---|
824 | Args as for the macro `proof-defstringset', except will be evaluated." |
---|
825 | (eval |
---|
826 | `(defun ,(if othername othername |
---|
827 | (intern (concat (symbol-name var) "-stringset"))) (arg) |
---|
828 | ,(concat "Set `" (symbol-name var) "' to ARG. |
---|
829 | This function simply uses customize-set-variable to set the variable. |
---|
830 | It was constructed with `proof-defstringset-fn'.") |
---|
831 | (interactive ,(format "sValue for %s (a string): " |
---|
832 | (symbol-name var))) |
---|
833 | (customize-set-variable (quote ,var) arg)))) |
---|
834 | |
---|
835 | (defmacro proof-defstringset (var &optional othername) |
---|
836 | "The setting function uses customize-set-variable to change the variable. |
---|
837 | OTHERNAME gives an alternative name than the default <VAR>-stringset. |
---|
838 | The name of the defined function is returned." |
---|
839 | `(proof-defstringset-fn (quote ,var) (quote ,othername))) |
---|
840 | |
---|
841 | |
---|
842 | |
---|
843 | ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |
---|
844 | ;;; |
---|
845 | ;;; Interface to custom lib |
---|
846 | ;;; |
---|
847 | |
---|
848 | ;; EMACSFIXME: A function that custom ought to provide. |
---|
849 | (defun pg-custom-save-vars (&rest variables) |
---|
850 | "Save custom vars VARIABLES." |
---|
851 | (dolist (symbol variables) |
---|
852 | (let ((value (get symbol 'customized-value))) |
---|
853 | ;; This code from customize-save-customized adjusts |
---|
854 | ;; properties so that custom-save-all will save |
---|
855 | ;; the value. |
---|
856 | (when value |
---|
857 | (put symbol 'saved-value value) |
---|
858 | (if (fboundp 'custom-push-theme) ;; XEmacs customize |
---|
859 | (custom-push-theme 'theme-value symbol 'user 'set value)) |
---|
860 | (put symbol 'customized-value nil)))) |
---|
861 | (custom-save-all)) |
---|
862 | |
---|
863 | ;; FIXME: this doesn't do quite same thing as reset button, |
---|
864 | ;; which *removes* a setting from `custom-set-variables' list |
---|
865 | ;; in custom.el. Instead, this adds something to a |
---|
866 | ;; custom-reset-variables list. |
---|
867 | (defun pg-custom-reset-vars (&rest variables) |
---|
868 | "Reset custom vars VARIABLES to their default values." |
---|
869 | ;; FIXME: probably this XEmacs specific |
---|
870 | (apply 'custom-reset-variables |
---|
871 | (mapcar (lambda (var) (list var 'default)) |
---|
872 | variables))) |
---|
873 | |
---|
874 | |
---|
875 | ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |
---|
876 | ;; |
---|
877 | ;; Finding executables |
---|
878 | ;; |
---|
879 | |
---|
880 | (defun proof-locate-executable (progname &optional returnnopath extrapath) |
---|
881 | "Search for PROGNAME on PATH. Return the full path to PROGNAME, or nil. |
---|
882 | If RETURNNOPATH is non-nil, return PROGNAME even if we can't find a full path. |
---|
883 | EXTRAPATH is a list of extra path components" |
---|
884 | (or |
---|
885 | (cond |
---|
886 | ((fboundp 'executable-find) |
---|
887 | (let ((exec-path (append exec-path extrapath))) |
---|
888 | (executable-find progname))) |
---|
889 | ((fboundp 'locate-file) |
---|
890 | (locate-file progname |
---|
891 | (append (split-path (getenv "PATH")) extrapath) |
---|
892 | (if proof-running-on-win32 '(".exe")) |
---|
893 | 1))) |
---|
894 | (if returnnopath progname))) |
---|
895 | |
---|
896 | ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |
---|
897 | ;; |
---|
898 | ;; Stuff for developing PG, not needed for ordinary users really. |
---|
899 | ;; [Could consider moving this to a new file `proof-devel.el'] |
---|
900 | ;; |
---|
901 | |
---|
902 | (put 'proof-if-setting-configured 'lisp-indent-function 1) |
---|
903 | (put 'proof-define-assistant-command 'lisp-indent-function 'defun) |
---|
904 | (put 'proof-define-assistant-command-witharg 'lisp-indent-function 'defun) |
---|
905 | (put 'defpgcustom 'lisp-indent-function 'defun) |
---|
906 | (put 'proof-map-buffers 'lisp-indent-function 'defun) |
---|
907 | (put 'proof-with-current-buffer-if-exists 'lisp-indent-function 'defun) |
---|
908 | |
---|
909 | (defconst proof-extra-fls |
---|
910 | (list |
---|
911 | (list "^(\\(proof-def\\" |
---|
912 | ;; Variable like things |
---|
913 | "\\(asscustom)\\|" |
---|
914 | ;; Function like things |
---|
915 | "\\([^ \t\n\(\)]+\\)" |
---|
916 | ;; Any whitespace and declared object. |
---|
917 | "[ \t'\(]*" |
---|
918 | "\\([^ \t\n\)]+\\)?") |
---|
919 | '(1 font-lock-keyword-face) |
---|
920 | '(8 (cond ((match-beginning 3) 'font-lock-variable-name-face) |
---|
921 | ;; ((match-beginning 6) 'font-lock-type-face) |
---|
922 | (t 'font-lock-function-name-face)) |
---|
923 | nil t))) |
---|
924 | |
---|
925 | ;; This doesn't work for FSF's font lock, developers should use |
---|
926 | ;; XEmacs! (unless edebug is broken, which it is in my 21.4.12) |
---|
927 | (if (boundp 'lisp-font-lock-keywords) ; compatibility hack |
---|
928 | (setq lisp-font-lock-keywords |
---|
929 | (append proof-extra-fls |
---|
930 | lisp-font-lock-keywords))) |
---|
931 | |
---|
932 | (setq autoload-package-name "proof") |
---|
933 | (setq generated-autoload-file "proof-autoloads.el") |
---|
934 | |
---|
935 | ;; End of proof-utils.el |
---|
936 | (provide 'proof-utils) |
---|