--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/ProofGeneral/progname.patch Sat Nov 28 15:53:10 2009 +0100
@@ -0,0 +1,51 @@
+--- a/isar/isabelle-system.el 2008-07-17 00:37:36.000000000 +0200
++++ b/isar/isabelle-system.el 2009-11-28 15:44:06.000000000 +0100
+@@ -125,9 +125,6 @@
+ :type 'file
+ :group 'isabelle)
+
+-(defvar isabelle-prog-name nil
+- "Set from `isabelle-set-prog-name', has name of logic appended sometimes.")
+-
+ (defun isa-tool-list-logics ()
+ "Generate a list of available object logics."
+ (if (isa-set-isatool-command)
+@@ -177,7 +174,7 @@
+
+ (defun isabelle-set-prog-name (&optional filename)
+ "Make proper command line for running Isabelle.
+-This function sets `isabelle-prog-name' and `proof-prog-name'."
++This function sets `proof-prog-name' and `isar-prog-args'."
+ (let*
+ ;; The ISABELLE and PROOFGENERAL_LOGIC values (set when run
+ ;; under the interface wrapper script) indicate command line
+@@ -187,21 +184,20 @@
+ (getenv "ISABELLE") ; command line override
+ (isa-getenv "ISABELLE") ; choose to match isatool
+ "isabelle")) ; to
+- (isabelle-opts (getenv "ISABELLE_OPTIONS"))
+- (opts (concat " -PI" ;; Proof General + Isar
+- (if proof-shell-unicode " -m PGASCII" "")
+- (if (and isabelle-opts (not (equal isabelle-opts "")))
+- (concat " " isabelle-opts) "")))
++ (isabelle-opts (split-string (getenv "ISABELLE_OPTIONS")))
++ (opts (append (list "-PI") ;; Proof General + Isar
++ (if proof-shell-unicode (list "-m" "PGASCII") nil)
++ isabelle-opts))
+ (logic (or isabelle-chosen-logic
+ (getenv "PROOFGENERAL_LOGIC")))
+ (logicarg (if (and logic (not (equal logic "")))
+- (concat " " logic) "")))
++ (list logic) nil)))
+ (setq isabelle-chosen-logic-prev isabelle-chosen-logic)
+- (setq isabelle-prog-name (concat isabelle opts logicarg))
+- (setq proof-prog-name isabelle-prog-name)))
++ (setq isar-prog-args (append opts logicarg))
++ (setq proof-prog-name isabelle)))
+
+ (defun isabelle-choose-logic (logic)
+- "Adjust isabelle-prog-name and proof-prog-name for running LOGIC."
++ "Adjust proof-prog-name and isar-prog-args for running LOGIC."
+ (interactive
+ (list (completing-read
+ "Use logic: "