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
|
;;; proof-general.el --- PG init file for package.el and ELPA compatibility -*- lexical-binding: t; -*-
;; This file is part of Proof General.
;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh
;; Portions © Copyright 2003-2019 Free Software Foundation, Inc.
;; Portions © Copyright 2001-2017 Pierre Courtieu
;; Portions © Copyright 2010, 2016 Erik Martin-Dorel
;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews
;; Portions © Copyright 2015-2017 Clément Pit-Claudel
;; Author: Clément Pit-Claudel <clement.pitclaudel@live.com>
;; URL: https://proofgeneral.github.io/
;; Package-Requires: ((emacs "24.3"))
;; Version: 4.5-git
;; This software is free software; you can redistribute it and/or
;; modify it under the terms of the GNU General Public License
;; version 2, as published by the Free Software Foundation.
;; This program is distributed in the hope that it will be useful,
;; but WITHOUT ANY WARRANTY; without even the implied warranty of
;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
;; GNU General Public License for more details.
;; You should have received a copy of the GNU General Public License
;; along with this program. If not, see <http://www.gnu.org/licenses/>.
;;; Commentary:
;;
;; Proof General's initialization code (in generic/proof-site) is relatively
;; complex, in part because it was written before package.el existed, and in
;; part because package.el still doesn't look for autoloads in subdirectories.
;; This file is a thin, package.el-friendly wrapper around generic/proof-site,
;; suitable for execution on Emacs start-up. It serves two purposes:
;;
;; * Setting up the load path when byte-compiling PG.
;; * Loading a minimal PG setup on startup (not all of Proof General, of course;
;; mostly mode hooks and autoloads).
;;; Code:
;;;###autoload
(if t (require 'proof-site
(expand-file-name "generic/proof-site"
(file-name-directory
(or load-file-name buffer-file-name)))))
(eval-when-compile
;; FIXME: This is used during installation of the ELPA package:
;; we presume that this file will be compiled before any of the files in
;; sub-directories and we presume that all files are compiled within the same
;; session, so we here add to load-path all the subdirectories so
;; that files in (say) coq/ can (require 'coq-foo) and the compiler will find
;; the corresponding file.
(let ((byte-compile-directories
'("generic" "lib"
"coq" "easycrypt" "pghaskell" "pgocaml" "pgshell" "phox"
;; FIXME: These dirs used to not be listed, but I needed to add
;; them for the compilation to succeed for me. --Stef
"isar" "lego" "twelf" "obsolete/plastic"))
(root (file-name-directory
(or load-file-name byte-compile-current-file buffer-file-name))))
(dolist (dir byte-compile-directories)
(add-to-list 'load-path (expand-file-name dir root)))))
(provide 'proof-general)
;;; proof-general.el ends here
|
