Admin/ProofGeneral/3.7.1.1/progname.patch
author blanchet
Mon, 19 May 2014 23:43:53 +0200
changeset 57005 33f3d2ea803d
parent 41639 d1cac8c778ed
permissions -rw-r--r--
store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution

--- a/isar/isabelle-system.el	2008-07-17 00:37:36.000000000 +0200
+++ b/isar/isabelle-system.el	2009-11-30 17:06:05.508481278 +0100
@@ -97,8 +97,8 @@
   (if (or proof-rsh-command
 	  (file-executable-p isa-isatool-command))
       (let ((setting (isa-shell-command-to-string
-		      (concat isa-isatool-command
-			      " getenv -b " envvar))))
+		      (concat "\"" isa-isatool-command
+			      "\" getenv -b " envvar))))
 	(if (string-equal setting "")
 	    default
 	  setting))
@@ -125,15 +125,12 @@
   :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)
       (delete "" (split-string
 		  (isa-shell-command-to-string
-		   (concat isa-isatool-command " findlogics")) "[ \t]"))))
+		   (concat "\"" isa-isatool-command "\" findlogics")) "[ \t]"))))
 
 (defcustom isabelle-logics-available nil
   "*List of logics available to use with Isabelle.
@@ -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: "
@@ -224,9 +220,7 @@
   (if (isa-set-isatool-command)
       (apply 'start-process
 	     "isa-view-doc" nil
-	     (append (split-string
-		      isa-isatool-command) 
-		     (list "doc" docname)))))
+	     (list isa-isatool-command "doc" docname))))
 
 (defun isa-tool-list-docs ()
   "Generate a list of documentation files available, with descriptions.
@@ -236,7 +230,7 @@
 passed to isa-tool-doc-command, DOCNAME will be viewed."
   (if (isa-set-isatool-command)
       (let ((docs (isa-shell-command-to-string
-		   (concat isa-isatool-command " doc"))))
+		   (concat "\"" isa-isatool-command "\" doc"))))
 	(unless (string-equal docs "")
 	  (mapcan
 	   (function (lambda (docdes)