author | wenzelm |
Wed, 02 Oct 2013 19:43:58 +0200 | |
changeset 54037 | ab77ec347220 |
parent 41639 | d1cac8c778ed |
permissions | -rw-r--r-- |
33911 | 1 |
--- a/isar/isabelle-system.el 2008-07-17 00:37:36.000000000 +0200 |
33927
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset
|
2 |
+++ b/isar/isabelle-system.el 2009-11-30 17:06:05.508481278 +0100 |
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset
|
3 |
@@ -97,8 +97,8 @@ |
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset
|
4 |
(if (or proof-rsh-command |
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset
|
5 |
(file-executable-p isa-isatool-command)) |
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset
|
6 |
(let ((setting (isa-shell-command-to-string |
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset
|
7 |
- (concat isa-isatool-command |
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset
|
8 |
- " getenv -b " envvar)))) |
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset
|
9 |
+ (concat "\"" isa-isatool-command |
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset
|
10 |
+ "\" getenv -b " envvar)))) |
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset
|
11 |
(if (string-equal setting "") |
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset
|
12 |
default |
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset
|
13 |
setting)) |
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset
|
14 |
@@ -125,15 +125,12 @@ |
33911 | 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) |
|
33927
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset
|
24 |
(delete "" (split-string |
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset
|
25 |
(isa-shell-command-to-string |
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset
|
26 |
- (concat isa-isatool-command " findlogics")) "[ \t]")))) |
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset
|
27 |
+ (concat "\"" isa-isatool-command "\" findlogics")) "[ \t]")))) |
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset
|
28 |
|
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset
|
29 |
(defcustom isabelle-logics-available nil |
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset
|
30 |
"*List of logics available to use with Isabelle. |
33911 | 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: " |
|
33927
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset
|
70 |
@@ -224,9 +220,7 @@ |
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset
|
71 |
(if (isa-set-isatool-command) |
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset
|
72 |
(apply 'start-process |
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset
|
73 |
"isa-view-doc" nil |
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset
|
74 |
- (append (split-string |
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset
|
75 |
- isa-isatool-command) |
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset
|
76 |
- (list "doc" docname))))) |
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset
|
77 |
+ (list isa-isatool-command "doc" docname)))) |
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset
|
78 |
|
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset
|
79 |
(defun isa-tool-list-docs () |
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset
|
80 |
"Generate a list of documentation files available, with descriptions. |
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset
|
81 |
@@ -236,7 +230,7 @@ |
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset
|
82 |
passed to isa-tool-doc-command, DOCNAME will be viewed." |
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset
|
83 |
(if (isa-set-isatool-command) |
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset
|
84 |
(let ((docs (isa-shell-command-to-string |
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset
|
85 |
- (concat isa-isatool-command " doc")))) |
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset
|
86 |
+ (concat "\"" isa-isatool-command "\" doc")))) |
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset
|
87 |
(unless (string-equal docs "") |
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset
|
88 |
(mapcan |
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset
|
89 |
(function (lambda (docdes) |