1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/Admin/ProofGeneral/progname.patch	Sat Nov 28 15:53:10 2009 +0100
     1.3 @@ -0,0 +1,51 @@
     1.4 +--- a/isar/isabelle-system.el	2008-07-17 00:37:36.000000000 +0200
     1.5 ++++ b/isar/isabelle-system.el	2009-11-28 15:44:06.000000000 +0100
     1.6 +@@ -125,9 +125,6 @@
     1.7 +   :type 'file
     1.8 +   :group 'isabelle)
     1.9 + 
    1.10 +-(defvar isabelle-prog-name nil
    1.11 +-  "Set from `isabelle-set-prog-name', has name of logic appended sometimes.")
    1.12 +-
    1.13 + (defun isa-tool-list-logics ()
    1.14 +   "Generate a list of available object logics."
    1.15 +   (if (isa-set-isatool-command)
    1.16 +@@ -177,7 +174,7 @@
    1.17 + 
    1.18 + (defun isabelle-set-prog-name (&optional filename)
    1.19 +   "Make proper command line for running Isabelle.
    1.20 +-This function sets `isabelle-prog-name' and `proof-prog-name'."
    1.21 ++This function sets `proof-prog-name' and `isar-prog-args'."
    1.22 +   (let*
    1.23 +       ;; The ISABELLE and PROOFGENERAL_LOGIC values (set when run
    1.24 +       ;; under the interface wrapper script) indicate command line
    1.25 +@@ -187,21 +184,20 @@
    1.26 + 		  (getenv "ISABELLE")	  ; command line override 
    1.27 + 		  (isa-getenv "ISABELLE") ; choose to match isatool
    1.28 + 		  "isabelle"))		  ; to 
    1.29 +-       (isabelle-opts (getenv "ISABELLE_OPTIONS"))
    1.30 +-       (opts (concat " -PI"  ;; Proof General + Isar
    1.31 +-	      (if proof-shell-unicode " -m PGASCII" "")
    1.32 +-	      (if (and isabelle-opts (not (equal isabelle-opts "")))
    1.33 +-		  (concat " " isabelle-opts) "")))
    1.34 ++       (isabelle-opts (split-string (getenv "ISABELLE_OPTIONS")))
    1.35 ++       (opts (append (list "-PI")  ;; Proof General + Isar
    1.36 ++		     (if proof-shell-unicode (list "-m" "PGASCII") nil)
    1.37 ++		     isabelle-opts))
    1.38 +        (logic (or isabelle-chosen-logic
    1.39 + 		  (getenv "PROOFGENERAL_LOGIC")))
    1.40 +        (logicarg (if (and logic (not (equal logic "")))
    1.41 +-		     (concat " " logic) "")))
    1.42 ++		     (list logic) nil)))
    1.43 +     (setq isabelle-chosen-logic-prev isabelle-chosen-logic)
    1.44 +-    (setq isabelle-prog-name (concat isabelle opts logicarg))
    1.45 +-    (setq proof-prog-name isabelle-prog-name)))
    1.46 ++    (setq isar-prog-args (append opts logicarg))
    1.47 ++    (setq proof-prog-name isabelle)))
    1.48 + 
    1.49 + (defun isabelle-choose-logic (logic)
    1.50 +-  "Adjust isabelle-prog-name and proof-prog-name for running LOGIC."
    1.51 ++  "Adjust proof-prog-name and isar-prog-args for running LOGIC."
    1.52 +   (interactive
    1.53 +    (list (completing-read
    1.54 + 	  "Use logic: "