33911
|
1 |
--- a/isar/isabelle-system.el 2008-07-17 00:37:36.000000000 +0200
|
|
2 |
+++ b/isar/isabelle-system.el 2009-11-28 15:44:06.000000000 +0100
|
|
3 |
@@ -125,9 +125,6 @@
|
|
4 |
:type 'file
|
|
5 |
:group 'isabelle)
|
|
6 |
|
|
7 |
-(defvar isabelle-prog-name nil
|
|
8 |
- "Set from `isabelle-set-prog-name', has name of logic appended sometimes.")
|
|
9 |
-
|
|
10 |
(defun isa-tool-list-logics ()
|
|
11 |
"Generate a list of available object logics."
|
|
12 |
(if (isa-set-isatool-command)
|
|
13 |
@@ -177,7 +174,7 @@
|
|
14 |
|
|
15 |
(defun isabelle-set-prog-name (&optional filename)
|
|
16 |
"Make proper command line for running Isabelle.
|
|
17 |
-This function sets `isabelle-prog-name' and `proof-prog-name'."
|
|
18 |
+This function sets `proof-prog-name' and `isar-prog-args'."
|
|
19 |
(let*
|
|
20 |
;; The ISABELLE and PROOFGENERAL_LOGIC values (set when run
|
|
21 |
;; under the interface wrapper script) indicate command line
|
|
22 |
@@ -187,21 +184,20 @@
|
|
23 |
(getenv "ISABELLE") ; command line override
|
|
24 |
(isa-getenv "ISABELLE") ; choose to match isatool
|
|
25 |
"isabelle")) ; to
|
|
26 |
- (isabelle-opts (getenv "ISABELLE_OPTIONS"))
|
|
27 |
- (opts (concat " -PI" ;; Proof General + Isar
|
|
28 |
- (if proof-shell-unicode " -m PGASCII" "")
|
|
29 |
- (if (and isabelle-opts (not (equal isabelle-opts "")))
|
|
30 |
- (concat " " isabelle-opts) "")))
|
|
31 |
+ (isabelle-opts (split-string (getenv "ISABELLE_OPTIONS")))
|
|
32 |
+ (opts (append (list "-PI") ;; Proof General + Isar
|
|
33 |
+ (if proof-shell-unicode (list "-m" "PGASCII") nil)
|
|
34 |
+ isabelle-opts))
|
|
35 |
(logic (or isabelle-chosen-logic
|
|
36 |
(getenv "PROOFGENERAL_LOGIC")))
|
|
37 |
(logicarg (if (and logic (not (equal logic "")))
|
|
38 |
- (concat " " logic) "")))
|
|
39 |
+ (list logic) nil)))
|
|
40 |
(setq isabelle-chosen-logic-prev isabelle-chosen-logic)
|
|
41 |
- (setq isabelle-prog-name (concat isabelle opts logicarg))
|
|
42 |
- (setq proof-prog-name isabelle-prog-name)))
|
|
43 |
+ (setq isar-prog-args (append opts logicarg))
|
|
44 |
+ (setq proof-prog-name isabelle)))
|
|
45 |
|
|
46 |
(defun isabelle-choose-logic (logic)
|
|
47 |
- "Adjust isabelle-prog-name and proof-prog-name for running LOGIC."
|
|
48 |
+ "Adjust proof-prog-name and isar-prog-args for running LOGIC."
|
|
49 |
(interactive
|
|
50 |
(list (completing-read
|
|
51 |
"Use logic: "
|