|
1 --- a/isar/isabelle-system.el 2008-07-17 00:37:36.000000000 +0200 |
|
2 +++ b/isar/isabelle-system.el 2009-11-30 17:06:05.508481278 +0100 |
|
3 @@ -97,8 +97,8 @@ |
|
4 (if (or proof-rsh-command |
|
5 (file-executable-p isa-isatool-command)) |
|
6 (let ((setting (isa-shell-command-to-string |
|
7 - (concat isa-isatool-command |
|
8 - " getenv -b " envvar)))) |
|
9 + (concat "\"" isa-isatool-command |
|
10 + "\" getenv -b " envvar)))) |
|
11 (if (string-equal setting "") |
|
12 default |
|
13 setting)) |
|
14 @@ -125,15 +125,12 @@ |
|
15 :type 'file |
|
16 :group 'isabelle) |
|
17 |
|
18 -(defvar isabelle-prog-name nil |
|
19 - "Set from `isabelle-set-prog-name', has name of logic appended sometimes.") |
|
20 - |
|
21 (defun isa-tool-list-logics () |
|
22 "Generate a list of available object logics." |
|
23 (if (isa-set-isatool-command) |
|
24 (delete "" (split-string |
|
25 (isa-shell-command-to-string |
|
26 - (concat isa-isatool-command " findlogics")) "[ \t]")))) |
|
27 + (concat "\"" isa-isatool-command "\" findlogics")) "[ \t]")))) |
|
28 |
|
29 (defcustom isabelle-logics-available nil |
|
30 "*List of logics available to use with Isabelle. |
|
31 @@ -177,7 +174,7 @@ |
|
32 |
|
33 (defun isabelle-set-prog-name (&optional filename) |
|
34 "Make proper command line for running Isabelle. |
|
35 -This function sets `isabelle-prog-name' and `proof-prog-name'." |
|
36 +This function sets `proof-prog-name' and `isar-prog-args'." |
|
37 (let* |
|
38 ;; The ISABELLE and PROOFGENERAL_LOGIC values (set when run |
|
39 ;; under the interface wrapper script) indicate command line |
|
40 @@ -187,21 +184,20 @@ |
|
41 (getenv "ISABELLE") ; command line override |
|
42 (isa-getenv "ISABELLE") ; choose to match isatool |
|
43 "isabelle")) ; to |
|
44 - (isabelle-opts (getenv "ISABELLE_OPTIONS")) |
|
45 - (opts (concat " -PI" ;; Proof General + Isar |
|
46 - (if proof-shell-unicode " -m PGASCII" "") |
|
47 - (if (and isabelle-opts (not (equal isabelle-opts ""))) |
|
48 - (concat " " isabelle-opts) ""))) |
|
49 + (isabelle-opts (split-string (getenv "ISABELLE_OPTIONS"))) |
|
50 + (opts (append (list "-PI") ;; Proof General + Isar |
|
51 + (if proof-shell-unicode (list "-m" "PGASCII") nil) |
|
52 + isabelle-opts)) |
|
53 (logic (or isabelle-chosen-logic |
|
54 (getenv "PROOFGENERAL_LOGIC"))) |
|
55 (logicarg (if (and logic (not (equal logic ""))) |
|
56 - (concat " " logic) ""))) |
|
57 + (list logic) nil))) |
|
58 (setq isabelle-chosen-logic-prev isabelle-chosen-logic) |
|
59 - (setq isabelle-prog-name (concat isabelle opts logicarg)) |
|
60 - (setq proof-prog-name isabelle-prog-name))) |
|
61 + (setq isar-prog-args (append opts logicarg)) |
|
62 + (setq proof-prog-name isabelle))) |
|
63 |
|
64 (defun isabelle-choose-logic (logic) |
|
65 - "Adjust isabelle-prog-name and proof-prog-name for running LOGIC." |
|
66 + "Adjust proof-prog-name and isar-prog-args for running LOGIC." |
|
67 (interactive |
|
68 (list (completing-read |
|
69 "Use logic: " |
|
70 @@ -224,9 +220,7 @@ |
|
71 (if (isa-set-isatool-command) |
|
72 (apply 'start-process |
|
73 "isa-view-doc" nil |
|
74 - (append (split-string |
|
75 - isa-isatool-command) |
|
76 - (list "doc" docname))))) |
|
77 + (list isa-isatool-command "doc" docname)))) |
|
78 |
|
79 (defun isa-tool-list-docs () |
|
80 "Generate a list of documentation files available, with descriptions. |
|
81 @@ -236,7 +230,7 @@ |
|
82 passed to isa-tool-doc-command, DOCNAME will be viewed." |
|
83 (if (isa-set-isatool-command) |
|
84 (let ((docs (isa-shell-command-to-string |
|
85 - (concat isa-isatool-command " doc")))) |
|
86 + (concat "\"" isa-isatool-command "\" doc")))) |
|
87 (unless (string-equal docs "") |
|
88 (mapcan |
|
89 (function (lambda (docdes) |