33911

1 
 a/isar/isabellesystem.el 20080717 00:37:36.000000000 +0200


2 
+++ b/isar/isabellesystem.el 20091128 15:44:06.000000000 +0100


3 
@@ 125,9 +125,6 @@


4 
:type 'file


5 
:group 'isabelle)


6 


7 
(defvar isabelleprogname nil


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


9 



10 
(defun isatoollistlogics ()


11 
"Generate a list of available object logics."


12 
(if (isasetisatoolcommand)


13 
@@ 177,7 +174,7 @@


14 


15 
(defun isabellesetprogname (&optional filename)


16 
"Make proper command line for running Isabelle.


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


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


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


25 
"isabelle")) ; to


26 
 (isabelleopts (getenv "ISABELLE_OPTIONS"))


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


28 
 (if proofshellunicode " m PGASCII" "")


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


30 
 (concat " " isabelleopts) "")))


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


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


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


34 
+ isabelleopts))


35 
(logic (or isabellechosenlogic


36 
(getenv "PROOFGENERAL_LOGIC")))


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


38 
 (concat " " logic) "")))


39 
+ (list logic) nil)))


40 
(setq isabellechosenlogicprev isabellechosenlogic)


41 
 (setq isabelleprogname (concat isabelle opts logicarg))


42 
 (setq proofprogname isabelleprogname)))


43 
+ (setq isarprogargs (append opts logicarg))


44 
+ (setq proofprogname isabelle)))


45 


46 
(defun isabellechooselogic (logic)


47 
 "Adjust isabelleprogname and proofprogname for running LOGIC."


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


49 
(interactive


50 
(list (completingread


51 
"Use logic: "
