author  blanchet 
Mon, 19 May 2014 23:43:53 +0200  
changeset 57005  33f3d2ea803d 
parent 41639  d1cac8c778ed 
permissions  rwrr 
33911  1 
 a/isar/isabellesystem.el 20080717 00:37:36.000000000 +0200 
33927
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset

2 
+++ b/isar/isabellesystem.el 20091130 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 proofrshcommand 
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset

5 
(fileexecutablep isaisatoolcommand)) 
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset

6 
(let ((setting (isashellcommandtostring 
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset

7 
 (concat isaisatoolcommand 
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 "\"" isaisatoolcommand 
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 (stringequal 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 isabelleprogname nil 

19 
 "Set from `isabellesetprogname', has name of logic appended sometimes.") 

20 
 

21 
(defun isatoollistlogics () 

22 
"Generate a list of available object logics." 

23 
(if (isasetisatoolcommand) 

33927
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset

24 
(delete "" (splitstring 
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset

25 
(isashellcommandtostring 
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset

26 
 (concat isaisatoolcommand " findlogics")) "[ \t]")))) 
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset

27 
+ (concat "\"" isaisatoolcommand "\" 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 isabellelogicsavailable 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 isabellesetprogname (&optional filename) 

34 
"Make proper command line for running Isabelle. 

35 
This function sets `isabelleprogname' and `proofprogname'." 

36 
+This function sets `proofprogname' and `isarprogargs'." 

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 
(isagetenv "ISABELLE") ; choose to match isatool 

43 
"isabelle")) ; to 

44 
 (isabelleopts (getenv "ISABELLE_OPTIONS")) 

45 
 (opts (concat " PI" ;; Proof General + Isar 

46 
 (if proofshellunicode " m PGASCII" "") 

47 
 (if (and isabelleopts (not (equal isabelleopts ""))) 

48 
 (concat " " isabelleopts) ""))) 

49 
+ (isabelleopts (splitstring (getenv "ISABELLE_OPTIONS"))) 

50 
+ (opts (append (list "PI") ;; Proof General + Isar 

51 
+ (if proofshellunicode (list "m" "PGASCII") nil) 

52 
+ isabelleopts)) 

53 
(logic (or isabellechosenlogic 

54 
(getenv "PROOFGENERAL_LOGIC"))) 

55 
(logicarg (if (and logic (not (equal logic ""))) 

56 
 (concat " " logic) ""))) 

57 
+ (list logic) nil))) 

58 
(setq isabellechosenlogicprev isabellechosenlogic) 

59 
 (setq isabelleprogname (concat isabelle opts logicarg)) 

60 
 (setq proofprogname isabelleprogname))) 

61 
+ (setq isarprogargs (append opts logicarg)) 

62 
+ (setq proofprogname isabelle))) 

63 

64 
(defun isabellechooselogic (logic) 

65 
 "Adjust isabelleprogname and proofprogname for running LOGIC." 

66 
+ "Adjust proofprogname and isarprogargs for running LOGIC." 

67 
(interactive 

68 
(list (completingread 

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 (isasetisatoolcommand) 
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset

72 
(apply 'startprocess 
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset

73 
"isaviewdoc" nil 
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset

74 
 (append (splitstring 
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset

75 
 isaisatoolcommand) 
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 isaisatoolcommand "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 isatoollistdocs () 
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 isatooldoccommand, DOCNAME will be viewed." 
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset

83 
(if (isasetisatoolcommand) 
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset

84 
(let ((docs (isashellcommandtostring 
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset

85 
 (concat isaisatoolcommand " doc")))) 
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset

86 
+ (concat "\"" isaisatoolcommand "\" doc")))) 
2a4c44b06eb4
more robust treatment of spaces in directory names;
wenzelm
parents:
33911
diff
changeset

87 
(unless (stringequal 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) 