blob: 59fa03c33aed22a141f26c9b4c67508635ef32e6 (
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
|
;;; proof.el --- Proof General loader.
;;
;; Copyright (C) 1998-2009 LFCS Edinburgh.
;; Authors: David Aspinall, Yves Bertot, Healfdene Goguen,
;; Thomas Kleymann and Dilip Sequeira
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
;;
;; $Id$
;;
;;; Commentary:
;;
;; This file loads Proof General. It is required by the
;; individual prover modes. Loading order of PG is:
;;
;; 1. proof-site (variables, autoloads & stubs for mode functions)
;; 2. stub <PA>-mode function sets proof-assistant-symbol and related variables
;; 3. prover-dependent variables defined in pg-custom
;; 4. stub explicitly loads <PA>/<PA>.el and execute real mode function
;; 5. <PA>.el requires this file, rest of PG loaded here
;; 6. further modules loaded by autoloads/prover-specific requires.
;;
;;
;;; Code:
(eval-when-compile
(require 'cl))
(eval-when (eval load compile)
(require 'proof-site) ; site/prover config, global vars, autoloads
(require 'proof-compat) ; Emacs and OS compatibility
(require 'proof-utils) ; utilities
(require 'proof-config) ; configuration variables
(unless noninteractive
(proof-splash-message)) ; welcome the user now.
(require 'proof-auxmodes) ; Further autoloads
)
(provide 'proof)
;;; proof.el ends here
|
