# HG changeset patch
# User wenzelm
# Date 1259419990 -3600
# Node ID 7c1764342cc8c1fb510a95f7e9a345890bf03ea6
# Parent  bae240a8bfe97a1c3036f55b5bfdab32433a8298
allow spaces within command-line arguments;

diff -r bae240a8bfe9 -r 7c1764342cc8 Admin/ProofGeneral/progname.patch
--- /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: "