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
|
;; proof-easy-config.el Easy configuration for Proof General
;;
;; Copyright (C) 1999 David Aspinall / LFCS.
;; Author: David Aspinall <da@dcs.ed.ac.uk>
;; Maintainer: Proof General maintainer <proofgen@dcs.ed.ac.uk>
;;
;; $Id$
;;
;; Work in progress.
;;
;; XEmacs only at the moment (uses defvaralias)
;;
;; Future version might copy settings instead. Consider how best to
;; interface with customization mechanism so a new prover can be
;; configured by editing inside custom buffers.
;;
(unless (fboundp 'defvaralias)
(error "proof-easy-config only works for XEmacs, sorry!"))
(defun proof-easy-config-make-var-aliases (sym group)
"Make variable aliases for custom GROUP, with new prefix SYM."
(let ((vars (custom-group-members group nil))
(prefix (length
(or (get 'custom-prefix group) ; fails sometimes, why?
"proof-"))) ; common prefix
(newpref (concat (symbol-name sym) "-")))
(dolist (cusmem vars)
(cond ((member 'custom-group cusmem)
;; recurse on subgroups
(proof-easy-config-make-var-aliases sym (car cusmem)))
((member 'custom-variable cusmem)
(let* ((thisone (car cusmem))
(base (substring (symbol-name thisone) prefix))
(alias (intern (concat newpref base))))
(defvaralias alias thisone)))))))
(defvar proof-easy-config-derived-modes-table
'(("" "script" proof-mode (proof-config-done))
("shell" "shell" proof-shell-mode (proof-shell-config-done))
("response" "resp" proof-response-mode (proof-response-config-done))
("goals" "goals" pbp-mode (proof-goals-config-done)))
"A list of (PREFIXSYM SUFFIXNAME PARENT MODEBODY) for derived modes.")
;; FIXME: Non-uniformity in current code
(defvaralias proof-mode-for-goals proof-mode-for-pbp)
(defun proof-easy-config-define-derived-modes ()
(dolist (modedef proof-easy-config-derived-modes-table)
(let* ((prefixsym (nth 1 modedef))
(suffixnm (nth 2 modedef))
(parent (nth 3 modedef))
(body (nthcdr 4 modedef))
(modert (concat proof-assistant-symbol "-" prefixsym))
(modecfgfn (intern (concat modert "config")))
(hyphen (if (string-equal prefixsym "") "" "-"))
(mode (intern (concat modert hyphen "mode")))
(fullbody (cons (list modecfgfn) body))
(modename (concat proof-assistant " " suffixnm))
(varname (intern (concat "proof-mode-for-" suffixnm))))
`(define-derived-mode ,mode ,parent ,modename nil ,@fullbody)
;; A hook into the mode body, before proof-config-done is
;; called. Probably unnecessary: the generic mode hook
;; functions would insert code in the same place.
`(defun ,modecfgfn ()
,(concat "Special configuration for " modert "mode.
You can redefine this function, currently it does nothing."))
;; Set proof-mode-for-script, etc. NB: at top-level rather
;; than in function body. Then we don't need to set
;; proof-pre-shell-start-hook.
`(setq ,varname ,mode))))
(defun proof-easy-config-define-customs ()
"Define a -prog-name customization setting."
(let ((pn-def (symbol-name proof-assistant-symbol))
(pn (intern (concat pn-def "-prog-name"))))
`(defcustom ,pn ,pn-def
,(concat "*Name of program to run " proof-assistant)
:type 'string
:group ,proof-assistant-symbol)
;; An alias which shadows ordinary proof-prog-name
(defvaralias 'proof-prog-name pn)))
(defmacro proof-easy-config (body)
"Configure Proof General for proof-assistant using settings in BODY."
`(progn
(proof-easy-config-make-var-aliases proof-assistant-symbol 'prover-config)
(proof-easy-config-define-customs)
,@body
(proof-easy-config-define-derived-modes)))
;;
(provide 'proof-easy-config)
|
