blob: e271cc99553ac8b9f298cea8d8098c97641a9480 (
plain)
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
|
;; proof.el Proof General loader.
;;
;; 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) ; site config
(require 'proof-config) ; variables
(if (string-match "XEmacs" emacs-version)
(require 'proof-splash)) ; splash screen
;; 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)))
;; Load toolbar code if toolbars available.
(if (featurep 'toolbar)
(require 'proof-toolbar))
;; Main code is in these files
(require 'proof-script)
(require 'proof-shell)
(provide 'proof)
;; proof.el ends here
|
