Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Admin/ProofGeneral/progname.patch
author huffman
Sun, 19 Dec 2010 06:59:01 -0800
changeset 41289 f655912ac235
parent 33927 2a4c44b06eb4
permissions -rw-r--r--
minimize imports; move domain class instances for powerdomain types into Powerdomains.thy
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
33927
2a4c44b06eb4 more robust treatment of spaces in directory names;
wenzelm
parents: 33911
diff changeset 
     2
 
+++ b/isar/isabelle-system.el	2009-11-30 17:06:05.508481278 +0100
2a4c44b06eb4 more robust treatment of spaces in directory names;
wenzelm
parents: 33911
diff changeset 
     3
 
@@ -97,8 +97,8 @@
2a4c44b06eb4 more robust treatment of spaces in directory names;
wenzelm
parents: 33911
diff changeset 
     4
 
   (if (or proof-rsh-command
2a4c44b06eb4 more robust treatment of spaces in directory names;
wenzelm
parents: 33911
diff changeset 
     5
 
 	  (file-executable-p isa-isatool-command))
2a4c44b06eb4 more robust treatment of spaces in directory names;
wenzelm
parents: 33911
diff changeset 
     6
 
       (let ((setting (isa-shell-command-to-string
2a4c44b06eb4 more robust treatment of spaces in directory names;
wenzelm
parents: 33911
diff changeset 
     7
 
-		      (concat isa-isatool-command
2a4c44b06eb4 more robust treatment of spaces in directory names;
wenzelm
parents: 33911
diff changeset 
     8
 
-			      " getenv -b " envvar))))
2a4c44b06eb4 more robust treatment of spaces in directory names;
wenzelm
parents: 33911
diff changeset 
     9
 
+		      (concat "\"" isa-isatool-command
2a4c44b06eb4 more robust treatment of spaces in directory names;
wenzelm
parents: 33911
diff changeset 
    10
 
+			      "\" getenv -b " envvar))))
2a4c44b06eb4 more robust treatment of spaces in directory names;
wenzelm
parents: 33911
diff changeset 
    11
 
 	(if (string-equal setting "")
2a4c44b06eb4 more robust treatment of spaces in directory names;
wenzelm
parents: 33911
diff changeset 
    12
 
 	    default
2a4c44b06eb4 more robust treatment of spaces in directory names;
wenzelm
parents: 33911
diff changeset 
    13
 
 	  setting))
2a4c44b06eb4 more robust treatment of spaces in directory names;
wenzelm
parents: 33911
diff changeset 
    14
 
@@ -125,15 +125,12 @@
33911
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    15
 
   :type 'file
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    16
 
   :group 'isabelle)
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    17
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    18
 
-(defvar isabelle-prog-name nil
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    19
 
-  "Set from `isabelle-set-prog-name', has name of logic appended sometimes.")
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    20
 
-
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    21
 
 (defun isa-tool-list-logics ()
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    22
 
   "Generate a list of available object logics."
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    23
 
   (if (isa-set-isatool-command)
33927
2a4c44b06eb4 more robust treatment of spaces in directory names;
wenzelm
parents: 33911
diff changeset 
    24
 
       (delete "" (split-string
2a4c44b06eb4 more robust treatment of spaces in directory names;
wenzelm
parents: 33911
diff changeset 
    25
 
 		  (isa-shell-command-to-string
2a4c44b06eb4 more robust treatment of spaces in directory names;
wenzelm
parents: 33911
diff changeset 
    26
 
-		   (concat isa-isatool-command " findlogics")) "[ \t]"))))
2a4c44b06eb4 more robust treatment of spaces in directory names;
wenzelm
parents: 33911
diff changeset 
    27
 
+		   (concat "\"" isa-isatool-command "\" findlogics")) "[ \t]"))))
2a4c44b06eb4 more robust treatment of spaces in directory names;
wenzelm
parents: 33911
diff changeset 
    28
2a4c44b06eb4 more robust treatment of spaces in directory names;
wenzelm
parents: 33911
diff changeset 
    29
 
 (defcustom isabelle-logics-available nil
2a4c44b06eb4 more robust treatment of spaces in directory names;
wenzelm
parents: 33911
diff changeset 
    30
 
   "*List of logics available to use with Isabelle.
33911
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    31
 
@@ -177,7 +174,7 @@
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    32
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    33
 
 (defun isabelle-set-prog-name (&optional filename)
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    34
 
   "Make proper command line for running Isabelle.
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    35
 
-This function sets `isabelle-prog-name' and `proof-prog-name'."
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    36
 
+This function sets `proof-prog-name' and `isar-prog-args'."
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    37
 
   (let*
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    38
 
       ;; The ISABELLE and PROOFGENERAL_LOGIC values (set when run
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    39
 
       ;; under the interface wrapper script) indicate command line
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    40
 
@@ -187,21 +184,20 @@
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    41
 
 		  (getenv "ISABELLE")	  ; command line override
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    42
 
 		  (isa-getenv "ISABELLE") ; choose to match isatool
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    43
 
 		  "isabelle"))		  ; to
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    44
 
-       (isabelle-opts (getenv "ISABELLE_OPTIONS"))
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    45
 
-       (opts (concat " -PI"  ;; Proof General + Isar
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    46
 
-	      (if proof-shell-unicode " -m PGASCII" "")
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    47
 
-	      (if (and isabelle-opts (not (equal isabelle-opts "")))
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    48
 
-		  (concat " " isabelle-opts) "")))
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    49
 
+       (isabelle-opts (split-string (getenv "ISABELLE_OPTIONS")))
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    50
 
+       (opts (append (list "-PI")  ;; Proof General + Isar
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    51
 
+		     (if proof-shell-unicode (list "-m" "PGASCII") nil)
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    52
 
+		     isabelle-opts))
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    53
 
        (logic (or isabelle-chosen-logic
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    54
 
 		  (getenv "PROOFGENERAL_LOGIC")))
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    55
 
        (logicarg (if (and logic (not (equal logic "")))
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    56
 
-		     (concat " " logic) "")))
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    57
 
+		     (list logic) nil)))
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    58
 
     (setq isabelle-chosen-logic-prev isabelle-chosen-logic)
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    59
 
-    (setq isabelle-prog-name (concat isabelle opts logicarg))
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    60
 
-    (setq proof-prog-name isabelle-prog-name)))
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    61
 
+    (setq isar-prog-args (append opts logicarg))
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    62
 
+    (setq proof-prog-name isabelle)))
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    63
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    64
 
 (defun isabelle-choose-logic (logic)
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    65
 
-  "Adjust isabelle-prog-name and proof-prog-name for running LOGIC."
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    66
 
+  "Adjust proof-prog-name and isar-prog-args for running LOGIC."
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    67
 
   (interactive
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    68
 
    (list (completing-read
7c1764342cc8 allow spaces within command-line arguments;
wenzelm
parents:
diff changeset 
    69
 
 	  "Use logic: "
33927
2a4c44b06eb4 more robust treatment of spaces in directory names;
wenzelm
parents: 33911
diff changeset 
    70
 
@@ -224,9 +220,7 @@
2a4c44b06eb4 more robust treatment of spaces in directory names;
wenzelm
parents: 33911
diff changeset 
    71
 
   (if (isa-set-isatool-command)
2a4c44b06eb4 more robust treatment of spaces in directory names;
wenzelm
parents: 33911
diff changeset 
    72
 
       (apply 'start-process
2a4c44b06eb4 more robust treatment of spaces in directory names;
wenzelm
parents: 33911
diff changeset 
    73
 
 	     "isa-view-doc" nil
2a4c44b06eb4 more robust treatment of spaces in directory names;
wenzelm
parents: 33911
diff changeset 
    74
 
-	     (append (split-string
2a4c44b06eb4 more robust treatment of spaces in directory names;
wenzelm
parents: 33911
diff changeset 
    75
 
-		      isa-isatool-command)
2a4c44b06eb4 more robust treatment of spaces in directory names;
wenzelm
parents: 33911
diff changeset 
    76
 
-		     (list "doc" docname)))))
2a4c44b06eb4 more robust treatment of spaces in directory names;
wenzelm
parents: 33911
diff changeset 
    77
 
+	     (list isa-isatool-command "doc" docname))))
2a4c44b06eb4 more robust treatment of spaces in directory names;
wenzelm
parents: 33911
diff changeset 
    78
2a4c44b06eb4 more robust treatment of spaces in directory names;
wenzelm
parents: 33911
diff changeset 
    79
 
 (defun isa-tool-list-docs ()
2a4c44b06eb4 more robust treatment of spaces in directory names;
wenzelm
parents: 33911
diff changeset 
    80
 
   "Generate a list of documentation files available, with descriptions.
2a4c44b06eb4 more robust treatment of spaces in directory names;
wenzelm
parents: 33911
diff changeset 
    81
 
@@ -236,7 +230,7 @@
2a4c44b06eb4 more robust treatment of spaces in directory names;
wenzelm
parents: 33911
diff changeset 
    82
 
 passed to isa-tool-doc-command, DOCNAME will be viewed."
2a4c44b06eb4 more robust treatment of spaces in directory names;
wenzelm
parents: 33911
diff changeset 
    83
 
   (if (isa-set-isatool-command)
2a4c44b06eb4 more robust treatment of spaces in directory names;
wenzelm
parents: 33911
diff changeset 
    84
 
       (let ((docs (isa-shell-command-to-string
2a4c44b06eb4 more robust treatment of spaces in directory names;
wenzelm
parents: 33911
diff changeset 
    85
 
-		   (concat isa-isatool-command " doc"))))
2a4c44b06eb4 more robust treatment of spaces in directory names;
wenzelm
parents: 33911
diff changeset 
    86
 
+		   (concat "\"" isa-isatool-command "\" doc"))))
2a4c44b06eb4 more robust treatment of spaces in directory names;
wenzelm
parents: 33911
diff changeset 
    87
 
 	(unless (string-equal docs "")
2a4c44b06eb4 more robust treatment of spaces in directory names;
wenzelm
parents: 33911
diff changeset 
    88
 
 	  (mapcan
2a4c44b06eb4 more robust treatment of spaces in directory names;
wenzelm
parents: 33911
diff changeset 
    89
 
 	   (function (lambda (docdes)
isabelle