blob: ae171aa0dab86b9a8d04af8be66066f120cc1953 (
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
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
|
;; File name: lclam.el
;; Description: Proof General instance for Lambda-CLAM
;; Author: James Brotherston <jjb@dai.ed.ac.uk>
;; Last modified: 23 October 2001
;;
;; $Id$
(require 'proof) ; load generic parts
(require 'proof-syntax)
;;
;; =========== User settings for Lambda-CLAM ============
;;
(defcustom lclam-prog-name ; "~/lambda-clam-teyjus/bin/lclam"
"lclam"
"*Name of program to run Lambda-CLAM"
:type 'file
:group 'lclam)
(defcustom lclam-web-page
"http://dream.dai.ed.ac.uk/software/systems/lambda-clam/"
"URL of web page for Lambda-CLAM"
:type 'string
:group 'lclam-config)
;;
;; =========== Configuration of generic modes ============
;;
(defun lclam-config ()
"Configure Proof General scripting for Lambda-CLAM."
(setq
proof-terminal-char ?\.
proof-comment-start "/*"
proof-comment-end "*/"
proof-goal-command-regexp "^pds_plan"
proof-save-command-regexp nil
proof-goal-with-hole-regexp nil
proof-save-with-hole-regexp nil
proof-non-undoables-regexp nil
proof-undo-n-times-cmd nil
proof-showproof-command nil
proof-goal-command "^pds_plan %s."
proof-save-command nil
proof-kill-goal-command nil
proof-assistant-homepage lclam-web-page
proof-auto-multiple-files nil
))
(defun lclam-shell-config ()
"Configure Proof General shell for Lambda-CLAM"
(setq
proof-shell-annotated-prompt-regexp "^lclam:"
proof-shell-cd-cmd nil
proof-shell-prompt-pattern nil
proof-shell-interrupt-regexp nil
proof-shell-error-regexp nil
proof-shell-start-goals-regexp nil
proof-shell-end-goals-regexp nil
proof-shell-proof-completed-regexp "^Plan Succeeded"
proof-shell-init-cmd nil
proof-shell-quit-cmd "halt."
proof-shell-eager-annotation-start nil
))
;;
;; =========== Defining the derived modes ================
;;
(define-derived-mode lclam-proofscript-mode proof-mode
"Lambda-CLAM script" nil
(lclam-config)
(proof-config-done))
(define-derived-mode lclam-shell-mode proof-shell-mode
"Lambda-CLAM shell" nil
(lclam-shell-config)
(proof-shell-config-done))
(define-derived-mode lclam-response-mode proof-response-mode
"Lambda-CLAM response" nil
(proof-response-config-done))
(define-derived-mode lclam-goals-mode proof-goals-mode
"Lambda-CLAM goals" nil
(proof-goals-config-done))
;; Automatic selection of theory file or proof script mode
;; .lcm -> proof script mode
;; .def -> theory file mode
(defun lclam-mode ()
(interactive)
(cond
((proof-string-match "\\.def$" (buffer-file-name))
(thy-mode))
(t
(lclam-proofscript-mode)))
)
;; Hook which configures settings to get the proof shell running
(add-hook 'proof-pre-shell-start-hook 'lclam-pre-shell-start)
(defun lclam-pre-shell-start ()
(setq proof-prog-name lclam-prog-name)
(setq proof-mode-for-shell 'lclam-shell-mode)
(setq proof-mode-for-response 'lclam-response-mode)
(setq proof-mode-for-goals 'lclam-goals-mode)
(setq proof-shell-process-connection-type t))
;;
;; ============ Extra bits and pieces - JB ============
;;
;; Open .def files in theory mode from now on
(setq auto-mode-alist
(cons '("\\.def$" . thy-mode) auto-mode-alist))
;; Remove redundant toolbar buttons
(setq lclam-toolbar-entries
(remassoc 'state lclam-toolbar-entries))
(setq lclam-toolbar-entries
(remassoc 'context lclam-toolbar-entries))
(setq lclam-toolbar-entries
(remassoc 'undo lclam-toolbar-entries))
(setq lclam-toolbar-entries
(remassoc 'retract lclam-toolbar-entries))
(setq lclam-toolbar-entries
(remassoc 'qed lclam-toolbar-entries))
;;
;; ============ Theory file mode ==============
;;
(define-derived-mode thy-mode fundamental-mode "Lambda-CLAM theory file mode"
(thy-add-menus))
(defvar thy-mode-map nil)
(defun thy-add-menus ()
"Add Lambda-CLAM menu to current menu bar."
(require 'proof-script)
(require 'proof-x-symbol)
(easy-menu-define thy-mode-pg-menu
thy-mode-map
"PG Menu for Lambda-CLAM Proof General"
(cons proof-general-name
(append
(list
;; A couple from the toolbar that make sense here
;; (also in proof-universal-keys)
["Issue command" proof-minibuffer-cmd t]
["Interrupt prover" proof-interrupt-process t])
(list proof-buffer-menu)
(list proof-help-menu))))
(easy-menu-define thy-mode-lclam-menu
thy-mode-map
"Menu for Lambda-CLAM Proof General, theory file mode."
(cons "Theory"
(list
["Next section" thy-goto-next-section t]
["Prev section" thy-goto-prev-section t]
["Insert template" thy-insert-template t]
; da: commented out this, function is incomplete
; ["Include definitions" match-and-assert-defs
; :active (proof-locked-region-empty-p)]
["Process theory" process-thy-file
:active (proof-locked-region-empty-p)]
; da: commented out this, there's no retract function provided
; ["Retract theory" isa-retract-thy-file
; :active (proof-locked-region-full-p)]
["Next error" proof-next-error t]
["Switch to script" thy-find-other-file t])))
(easy-menu-add thy-mode-pg-menu thy-mode-map)
(easy-menu-add thy-mode-lclam-menu thy-mode-map)
)
(defun process-thy-file (file)
"Process the theory file FILE. If interactive, use buffer-file-name."
(interactive (list buffer-file-name))
(save-some-buffers)
(update-thy-only file nil nil))
(defun update-thy-only (file try wait)
"Process the theory file FILE."
;; First make sure we're in the right directory to take care of
;; relative "files" paths inside theory file.
(proof-cd-sync)
(proof-shell-invisible-command
(proof-format-filename
;; %r parameter means relative (don't expand) path
(format "use_thy \"%%r\"." (if try "try_" ""))
(file-name-nondirectory file))
wait))
;(defun match-and-assert-defs
; "Interactively process and assert definitions in theory file"
;)
(provide 'lclam)
|
