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
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
|
;; isabelle-system.el Interface with Isabelle system
;;
;; Copyright (C) 2000 LFCS Edinburgh, David Aspinall.
;;
;; Author: David Aspinall <da@dcs.ed.ac.uk>
;; Maintainer: Proof General maintainer <proofgen@dcs.ed.ac.uk>
;;
;; $Id$
;;
;; Most of this code is taken from the final version of Isamode.
;; --------------------------------------------------------------
;;
(require 'proof)
;;; ================ Extract Isabelle settings ================
(defcustom isa-isatool-command
(or (getenv "ISATOOL")
(let ((possibilities
'("isatool"
"/usr/bin/isatool"
"/usr/local/bin/isatool"
"/usr/lib/Isabelle/bin/isatool"
"/usr/lib/Isabelle99/bin/isatool"
"/usr/share/Isabelle/bin/isatool"
"/usr/share/Isabelle99/bin/isatool")))
(while (and possibilities
(not (file-executable-p
(car possibilities))))
(setq possibilities (cdr possibilities)))
(car-safe possibilities))
"path_to_isatool_is_unknown")
"Command to invoke Isabelle tool 'isatool'.
Use a full path name here if isatool is not on PATH when Emacs is started."
:type 'file
:group 'isabelle)
(defun isa-set-isatool-command ()
"Make sure isa-isatool-command points to a valid executable.
If it does not, prompt the user for the proper setting.
If it appears we're running on win32, allow this to remain unset.
Returns non-nil if isa-isatool-command is valid."
(interactive)
(while (unless proof-running-on-win32
(not (file-executable-p isa-isatool-command)))
(beep)
(setq isa-isatool-command
(read-file-name
"Please type in the full path to the `isatool' program: "
nil nil t)))
(if (and proof-running-on-win32
(not (file-executable-p isa-isatool-command)))
(warning "Proof General: isatool command not found; ignored because Win32 system detected."))
(file-executable-p isa-isatool-command))
(defun isa-shell-command-to-string (command)
"Like shell-command-to-string except the last character is stripped."
(substring (shell-command-to-string command) 0 -1))
(defun isa-getenv (envvar &optional default)
"Extract an environment variable setting using the `isatool' program.
If the isatool command is not available, try using elisp's getenv
to extract the value from Emacs' environment.
If there is no setting for the variable, DEFAULT will be returned"
(isa-set-isatool-command)
(if (file-executable-p isa-isatool-command)
(let ((setting (isa-shell-command-to-string
(concat isa-isatool-command
" getenv -b " envvar))))
(if (string-equal setting "")
default
setting))
(or (getenv envvar) default)))
;;;
;;; ======= Interaction with System using Isabelle tools =======
;;;
(defcustom isabelle-prog-name
(if (fboundp 'win32-long-file-name)
"C:\\sml\\bin\\.run\\run.x86-win32.exe @SMLload=C:\\Isabelle\\"
"isabelle")
"*Default name of program to run Isabelle.
The default value except when running under Windows is \"isabelle\".
The default value when running under Windows is:
C:\\sml\\bin\\.run\\run.x86-win32.exe @SMLload=C:\\Isabelle\\
This expects SML/NJ in C:\\sml and Isabelle images in C:\Isabelle.
The logic image name is tagged onto the end.
NB: The Isabelle settings mechanism or the environment variable
ISABELLE will always override this setting."
:type 'file
:group 'isabelle)
(defun isa-tool-run-command (logic-name)
"Make a command for running Isabelle using Isabelle tools.
This function is called with the name of the logic as an argument,
and builds a program name and arguments to run Isabelle."
(let*
((default (if proof-running-on-win32
(concat isabelle-prog-name logic-name)
isabelle-prog-name))
(commd (isa-getenv "ISABELLE" default)))
(cond
(proof-running-on-win32 ; Assume no special font there
commd)
(isa-use-special-font
(concat commd "-misabelle_font" "-msymbols" logic-name))
(t
commd))))
(defun isa-tool-list-logics ()
"Generate a list of available object logics."
(if (isa-set-isatool-command)
(split-string (isa-shell-command-to-string
(concat isa-isatool-command " findlogics")) "[ \t]")))
(defun isa-view-doc (docname)
"View Isabelle document DOCNAME, using Isabelle tools."
(if (isa-set-isatool-command)
(apply 'start-process
"isa-view-doc" nil
(list isa-isatool-command "doc" docname))))
(defun isa-tool-list-docs ()
"Generate a list of documentation files available, with descriptions.
This function returns a list of lists of the form
((DOCNAME DESCRIPTION) ....)
of Isabelle document names and descriptions. When DOCNAME is
passed to isa-tool-doc-command, DOCNAME will be viewed."
(if (isa-set-isatool-command)
(mapcar
(function (lambda (docdes)
(list
(substring docdes (string-match "\\(\\S-+\\)[ \t]+" docdes)
(match-end 1))
(substring docdes (match-end 0)))))
(split-string
(isa-shell-command-to-string
(concat isa-isatool-command " doc")) "\n"))))
(defun isa-tool-setup-font ()
"Setup special font for isabelle, using Isabelle tools."
(isa-set-isatool-command)
(call-process isa-isatool-command nil nil nil "installfonts"))
(defun isa-default-logic-dir ()
"Return a directory containing logic images."
(car (split-string (isa-getenv "ISABELLE_PATH") ":")))
(defun isa-default-logic ()
"Return the default logic."
(or (isa-getenv "ISABELLE_LOGIC") "Pure"))
(defun isa-quit (save)
"Quit / save the Isabelle session.
Called with one argument: t to save database, nil otherwise."
(if (not save)
(isa-insert-ret "quit();"))
(comint-send-eof))
;;; ========== Utility functions ==========
;; FIXME: a way of updating this list, please?
(defcustom isabelle-logics-available (isa-tool-list-logics)
"*List of logics available to use with Isabelle.
If the `isatool' program is available, this is automatically
generated."
:type (list 'string)
:group 'isabelle)
;; FIXME: type here needs to be dynamic based on isabelle-logics-avalable
;; Is that possible?
;; Otherwise it should be updated on re-loading.
(defcustom isabelle-logic "HOL"
"*Choice of logic to use with Isabelle.
If non-nil, will be added into isabelle-prog-name as default value.
NB: you have saved a new logic image, it may not appear in the choices
until Proof General is restarted."
:type (append
(list 'choice)
(mapcar (lambda (str) (list 'const str)) isabelle-logics-available)
(list '(string :tag "Choose another")
'(const :tag "Unset (use default)" nil)))
:group 'isabelle)
(defvar isa-docs-menu
(let ((vc '(lambda (docdes)
(vector (car (cdr docdes))
(list 'isa-view-doc (car docdes)) t))))
(cons "Docs"
(append
; '(["Isamode info" (progn (require 'info)
; (Info-goto-node "(Isamode)Top")) t])
(mapcar vc (isa-tool-list-docs)))))
"Isabelle documentation menu. Constructed dynamically.")
;;; ========== Mirroring Proof General options in Isabelle process ========
;; NB: EXPERIMENTAL: to be generalised to all provers
(defcustom isabelle-show-types nil
"Whether to show types in Isabelle."
:type 'boolean
:set 'proof-set-value
:group 'isabelle)
(defun isabelle-show-types ()
(isa-proof-invisible-command-ifposs (isa-set-default-cmd 'isabelle-show-types)))
(defcustom isabelle-show-sorts nil
"Whether to show sorts in Isabelle."
:type 'boolean
:set 'proof-set-value
:group 'isabelle)
(defun isabelle-show-sorts ()
(isa-proof-invisible-command-ifposs (isa-set-default-cmd 'isabelle-show-sorts)))
(defun isa-proof-invisible-command-ifposs (cmd)
;; Better would be to queue the command, or even interrupt a queue
;; in progress. Also must send current settings at start
;; of session somehow. (This might happen automatically if
;; a queue of deffered commands is set, since defcustom calls
;; proof-set-value even to set the default/initial value?)
(if (proof-shell-available-p)
(progn
(proof-shell-invisible-command cmd t)
(proof-prf) ; refresh display, should only do if goals active.
)))
(defun isa-format-bool (string val)
(proof-format (list (cons "%b" (if val "true" "false"))) string))
(defcustom isa-default-values-list
'((isabelle-show-types . (isa-format-bool "show_types:=%b;" isabelle-show-types))
(isabelle-show-sorts . (isa-format-bool "show_sorts:=%b;" isabelle-show-sorts)))
"A list of default values kept in Proof General which are sent to Isabelle."
:type 'sexp
:group 'isabelle-config)
(defun isa-set-default-cmd (&optional setting)
"Return a string for setting default values kept in Proof General customizations.
If SETTING is non-nil, return a string for just that setting.
Otherwise return a string for configuring all settings."
(let
((evalifneeded (lambda (expr)
(if (or (not setting) (eq setting (car expr)))
(eval (cdr expr))))))
(apply 'concat (mapcar evalifneeded isa-default-values-list))))
(provide 'isabelle-system)
;; End of isabelle-system.el
|
