blob: 64ee3b6163537d7dab1336c7570b52c999deea2f (
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
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
|
;; proof-site.el --- Configuration for site and choice of prover.
;;
;; Copyright (C) 1994 - 1998 LFCS Edinburgh.
;; Authors: David Aspinall, Thomas Kleymann
;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk>
;;
;; $Id$
;;
;; FUTURE: in the future it might be nice to allow switching between
;; different proof assistants in the same session. Presently, the
;; code will only allow one assistant to be chosen for the whole
;; session.
;;
(or (featurep 'custom)
;; Quick hack to support defcustom for Emacs 19
(defmacro defcustom (sym val doc &rest args)
(defvar sym val doc))
(defmacro group (sym mems doc &rest args)))
(defgroup proof nil
"Customization of generic parameters for Proof General."
:group 'external
:group 'processes)
(defcustom proof-home
(or (getenv "PROOF_HOME") "~/devel/lego/elisp/")
"*Directory where Proof General is installed. Ends with slash.
Default value taken from PROOF_HOME, or use customize to set it."
:type 'directory
:group 'proof)
(defcustom proof-image-directory
(concat proof-home "images/")
"*Where Proof General image files are installed. Ends with slash."
:type 'directory
:group 'proof)
(defcustom proof-info-dir
(concat proof-home "doc/")
"*Where Proof General Info files are installed."
:type 'directory
:group 'proof)
;; Add the info directory to the end of Emacs Info path
;; if need be.
(or (memq proof-info-dir Info-default-directory-list)
(setq Info-default-directory-list
(append
Info-default-directory-list
(list proof-info-dir))))
(defcustom proof-assistants
'(isa lego coq)
"*Choice of proof assitants to use with Proof General.
A list of symbol chosen from: 'lego 'coq 'isa
NB: To change proof assistant, you must start a new Emacs session."
:type '(set (const :tag "Isabelle" isa)
(const :tag "LEGO" lego)
(const :tag "Coq" coq))
:group 'proof)
;; Extend load path
(setq load-path
(cons (concat proof-home "generic/") load-path))
;; Add auto-loads and load-path elements
;; to support the proof assistants selected
(let ((assistants proof-assistants) proof-assistant)
(while assistants
(let*
((proof-assistant (car assistants))
(fileregexp
(cond ((eq proof-assistant 'coq) "\\.v")
((eq proof-assistant 'lego) "\\.l$")
((eq proof-assistant 'isa) "\\.ML$\\|\\.thy$")))
(assistant-name (symbol-name proof-assistant))
(proof-mode (intern (concat assistant-name "-mode"))))
(setq auto-mode-alist
(cons (cons fileregexp proof-mode) auto-mode-alist))
;; NB: File name for each prover is the same as its symbol name!
(autoload proof-mode assistant-name
(concat
"Major mode for editing scripts for proof assistant " assistant-name ".")
t)
(setq load-path
(cons
(concat proof-home (symbol-name proof-assistant) "/")
load-path))
(setq assistants (cdr assistants))
)))
;; WARNING: do not edit below here
;; (the next constant is set automatically)
(defconst proof-general-version
"Proof General, Version 2.0-pre980910 released by da,tms. Email lego@dcs.ed.ac.uk."
"Version string for Proof General.")
(provide 'proof-site)
|
