Admin/ProofGeneral/progname.patch
author wenzelm
Sun, 29 Nov 2009 17:44:44 +0100
changeset 33922 639eb84ec640
parent 33911 7c1764342cc8
child 33927 2a4c44b06eb4
permissions -rw-r--r--
raised proof-shell-quit-timeout to accomodate bulky write-back images;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33911
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
     1
--- a/isar/isabelle-system.el	2008-07-17 00:37:36.000000000 +0200
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
     2
+++ b/isar/isabelle-system.el	2009-11-28 15:44:06.000000000 +0100
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
     3
@@ -125,9 +125,6 @@
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
     4
   :type 'file
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
     5
   :group 'isabelle)
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
     6
 
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
     7
-(defvar isabelle-prog-name nil
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
     8
-  "Set from `isabelle-set-prog-name', has name of logic appended sometimes.")
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
     9
-
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
    10
 (defun isa-tool-list-logics ()
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
    11
   "Generate a list of available object logics."
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
    12
   (if (isa-set-isatool-command)
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
    13
@@ -177,7 +174,7 @@
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
    14
 
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
    15
 (defun isabelle-set-prog-name (&optional filename)
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
    16
   "Make proper command line for running Isabelle.
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
    17
-This function sets `isabelle-prog-name' and `proof-prog-name'."
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
    18
+This function sets `proof-prog-name' and `isar-prog-args'."
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
    19
   (let*
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
    20
       ;; The ISABELLE and PROOFGENERAL_LOGIC values (set when run
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
    21
       ;; under the interface wrapper script) indicate command line
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
    22
@@ -187,21 +184,20 @@
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
    23
 		  (getenv "ISABELLE")	  ; command line override 
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
    24
 		  (isa-getenv "ISABELLE") ; choose to match isatool
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
    25
 		  "isabelle"))		  ; to 
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
    26
-       (isabelle-opts (getenv "ISABELLE_OPTIONS"))
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
    27
-       (opts (concat " -PI"  ;; Proof General + Isar
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
    28
-	      (if proof-shell-unicode " -m PGASCII" "")
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
    29
-	      (if (and isabelle-opts (not (equal isabelle-opts "")))
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
    30
-		  (concat " " isabelle-opts) "")))
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
    31
+       (isabelle-opts (split-string (getenv "ISABELLE_OPTIONS")))
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
    32
+       (opts (append (list "-PI")  ;; Proof General + Isar
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
    33
+		     (if proof-shell-unicode (list "-m" "PGASCII") nil)
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
    34
+		     isabelle-opts))
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
    35
        (logic (or isabelle-chosen-logic
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
    36
 		  (getenv "PROOFGENERAL_LOGIC")))
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
    37
        (logicarg (if (and logic (not (equal logic "")))
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
    38
-		     (concat " " logic) "")))
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
    39
+		     (list logic) nil)))
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
    40
     (setq isabelle-chosen-logic-prev isabelle-chosen-logic)
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
    41
-    (setq isabelle-prog-name (concat isabelle opts logicarg))
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
    42
-    (setq proof-prog-name isabelle-prog-name)))
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
    43
+    (setq isar-prog-args (append opts logicarg))
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
    44
+    (setq proof-prog-name isabelle)))
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
    45
 
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
    46
 (defun isabelle-choose-logic (logic)
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
    47
-  "Adjust isabelle-prog-name and proof-prog-name for running LOGIC."
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
    48
+  "Adjust proof-prog-name and isar-prog-args for running LOGIC."
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
    49
   (interactive
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
    50
    (list (completing-read
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset
    51
 	  "Use logic: "