1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/Admin/ProofGeneral/3.7.1.1/progname.patch Thu Jan 27 20:46:20 2011 +0100
1.3 @@ -0,0 +1,89 @@
1.4 +--- a/isar/isabelle-system.el 2008-07-17 00:37:36.000000000 +0200
1.5 ++++ b/isar/isabelle-system.el 2009-11-30 17:06:05.508481278 +0100
1.6 +@@ -97,8 +97,8 @@
1.7 + (if (or proof-rsh-command
1.8 + (file-executable-p isa-isatool-command))
1.9 + (let ((setting (isa-shell-command-to-string
1.10 +- (concat isa-isatool-command
1.11 +- " getenv -b " envvar))))
1.12 ++ (concat "\"" isa-isatool-command
1.13 ++ "\" getenv -b " envvar))))
1.14 + (if (string-equal setting "")
1.15 + default
1.16 + setting))
1.17 +@@ -125,15 +125,12 @@
1.18 + :type 'file
1.19 + :group 'isabelle)
1.20 +
1.21 +-(defvar isabelle-prog-name nil
1.22 +- "Set from `isabelle-set-prog-name', has name of logic appended sometimes.")
1.23 +-
1.24 + (defun isa-tool-list-logics ()
1.25 + "Generate a list of available object logics."
1.26 + (if (isa-set-isatool-command)
1.27 + (delete "" (split-string
1.28 + (isa-shell-command-to-string
1.29 +- (concat isa-isatool-command " findlogics")) "[ \t]"))))
1.30 ++ (concat "\"" isa-isatool-command "\" findlogics")) "[ \t]"))))
1.31 +
1.32 + (defcustom isabelle-logics-available nil
1.33 + "*List of logics available to use with Isabelle.
1.34 +@@ -177,7 +174,7 @@
1.35 +
1.36 + (defun isabelle-set-prog-name (&optional filename)
1.37 + "Make proper command line for running Isabelle.
1.38 +-This function sets `isabelle-prog-name' and `proof-prog-name'."
1.39 ++This function sets `proof-prog-name' and `isar-prog-args'."
1.40 + (let*
1.41 + ;; The ISABELLE and PROOFGENERAL_LOGIC values (set when run
1.42 + ;; under the interface wrapper script) indicate command line
1.43 +@@ -187,21 +184,20 @@
1.44 + (getenv "ISABELLE") ; command line override
1.45 + (isa-getenv "ISABELLE") ; choose to match isatool
1.46 + "isabelle")) ; to
1.47 +- (isabelle-opts (getenv "ISABELLE_OPTIONS"))
1.48 +- (opts (concat " -PI" ;; Proof General + Isar
1.49 +- (if proof-shell-unicode " -m PGASCII" "")
1.50 +- (if (and isabelle-opts (not (equal isabelle-opts "")))
1.51 +- (concat " " isabelle-opts) "")))
1.52 ++ (isabelle-opts (split-string (getenv "ISABELLE_OPTIONS")))
1.53 ++ (opts (append (list "-PI") ;; Proof General + Isar
1.54 ++ (if proof-shell-unicode (list "-m" "PGASCII") nil)
1.55 ++ isabelle-opts))
1.56 + (logic (or isabelle-chosen-logic
1.57 + (getenv "PROOFGENERAL_LOGIC")))
1.58 + (logicarg (if (and logic (not (equal logic "")))
1.59 +- (concat " " logic) "")))
1.60 ++ (list logic) nil)))
1.61 + (setq isabelle-chosen-logic-prev isabelle-chosen-logic)
1.62 +- (setq isabelle-prog-name (concat isabelle opts logicarg))
1.63 +- (setq proof-prog-name isabelle-prog-name)))
1.64 ++ (setq isar-prog-args (append opts logicarg))
1.65 ++ (setq proof-prog-name isabelle)))
1.66 +
1.67 + (defun isabelle-choose-logic (logic)
1.68 +- "Adjust isabelle-prog-name and proof-prog-name for running LOGIC."
1.69 ++ "Adjust proof-prog-name and isar-prog-args for running LOGIC."
1.70 + (interactive
1.71 + (list (completing-read
1.72 + "Use logic: "
1.73 +@@ -224,9 +220,7 @@
1.74 + (if (isa-set-isatool-command)
1.75 + (apply 'start-process
1.76 + "isa-view-doc" nil
1.77 +- (append (split-string
1.78 +- isa-isatool-command)
1.79 +- (list "doc" docname)))))
1.80 ++ (list isa-isatool-command "doc" docname))))
1.81 +
1.82 + (defun isa-tool-list-docs ()
1.83 + "Generate a list of documentation files available, with descriptions.
1.84 +@@ -236,7 +230,7 @@
1.85 + passed to isa-tool-doc-command, DOCNAME will be viewed."
1.86 + (if (isa-set-isatool-command)
1.87 + (let ((docs (isa-shell-command-to-string
1.88 +- (concat isa-isatool-command " doc"))))
1.89 ++ (concat "\"" isa-isatool-command "\" doc"))))
1.90 + (unless (string-equal docs "")
1.91 + (mapcan
1.92 + (function (lambda (docdes)