Admin/ProofGeneral/progname.patch
author blanchet
Tue Dec 07 11:56:53 2010 +0100 (2010-12-07)
changeset 41052 3db267a01c1d
parent 33927 2a4c44b06eb4
permissions -rw-r--r--
remove the "fin_fun" optimization in Nitpick -- it was always a hack and didn't help much
     1 --- a/isar/isabelle-system.el	2008-07-17 00:37:36.000000000 +0200
     2 +++ b/isar/isabelle-system.el	2009-11-30 17:06:05.508481278 +0100
     3 @@ -97,8 +97,8 @@
     4    (if (or proof-rsh-command
     5  	  (file-executable-p isa-isatool-command))
     6        (let ((setting (isa-shell-command-to-string
     7 -		      (concat isa-isatool-command
     8 -			      " getenv -b " envvar))))
     9 +		      (concat "\"" isa-isatool-command
    10 +			      "\" getenv -b " envvar))))
    11  	(if (string-equal setting "")
    12  	    default
    13  	  setting))
    14 @@ -125,15 +125,12 @@
    15    :type 'file
    16    :group 'isabelle)
    17  
    18 -(defvar isabelle-prog-name nil
    19 -  "Set from `isabelle-set-prog-name', has name of logic appended sometimes.")
    20 -
    21  (defun isa-tool-list-logics ()
    22    "Generate a list of available object logics."
    23    (if (isa-set-isatool-command)
    24        (delete "" (split-string
    25  		  (isa-shell-command-to-string
    26 -		   (concat isa-isatool-command " findlogics")) "[ \t]"))))
    27 +		   (concat "\"" isa-isatool-command "\" findlogics")) "[ \t]"))))
    28  
    29  (defcustom isabelle-logics-available nil
    30    "*List of logics available to use with Isabelle.
    31 @@ -177,7 +174,7 @@
    32  
    33  (defun isabelle-set-prog-name (&optional filename)
    34    "Make proper command line for running Isabelle.
    35 -This function sets `isabelle-prog-name' and `proof-prog-name'."
    36 +This function sets `proof-prog-name' and `isar-prog-args'."
    37    (let*
    38        ;; The ISABELLE and PROOFGENERAL_LOGIC values (set when run
    39        ;; under the interface wrapper script) indicate command line
    40 @@ -187,21 +184,20 @@
    41  		  (getenv "ISABELLE")	  ; command line override 
    42  		  (isa-getenv "ISABELLE") ; choose to match isatool
    43  		  "isabelle"))		  ; to 
    44 -       (isabelle-opts (getenv "ISABELLE_OPTIONS"))
    45 -       (opts (concat " -PI"  ;; Proof General + Isar
    46 -	      (if proof-shell-unicode " -m PGASCII" "")
    47 -	      (if (and isabelle-opts (not (equal isabelle-opts "")))
    48 -		  (concat " " isabelle-opts) "")))
    49 +       (isabelle-opts (split-string (getenv "ISABELLE_OPTIONS")))
    50 +       (opts (append (list "-PI")  ;; Proof General + Isar
    51 +		     (if proof-shell-unicode (list "-m" "PGASCII") nil)
    52 +		     isabelle-opts))
    53         (logic (or isabelle-chosen-logic
    54  		  (getenv "PROOFGENERAL_LOGIC")))
    55         (logicarg (if (and logic (not (equal logic "")))
    56 -		     (concat " " logic) "")))
    57 +		     (list logic) nil)))
    58      (setq isabelle-chosen-logic-prev isabelle-chosen-logic)
    59 -    (setq isabelle-prog-name (concat isabelle opts logicarg))
    60 -    (setq proof-prog-name isabelle-prog-name)))
    61 +    (setq isar-prog-args (append opts logicarg))
    62 +    (setq proof-prog-name isabelle)))
    63  
    64  (defun isabelle-choose-logic (logic)
    65 -  "Adjust isabelle-prog-name and proof-prog-name for running LOGIC."
    66 +  "Adjust proof-prog-name and isar-prog-args for running LOGIC."
    67    (interactive
    68     (list (completing-read
    69  	  "Use logic: "
    70 @@ -224,9 +220,7 @@
    71    (if (isa-set-isatool-command)
    72        (apply 'start-process
    73  	     "isa-view-doc" nil
    74 -	     (append (split-string
    75 -		      isa-isatool-command) 
    76 -		     (list "doc" docname)))))
    77 +	     (list isa-isatool-command "doc" docname))))
    78  
    79  (defun isa-tool-list-docs ()
    80    "Generate a list of documentation files available, with descriptions.
    81 @@ -236,7 +230,7 @@
    82  passed to isa-tool-doc-command, DOCNAME will be viewed."
    83    (if (isa-set-isatool-command)
    84        (let ((docs (isa-shell-command-to-string
    85 -		   (concat isa-isatool-command " doc"))))
    86 +		   (concat "\"" isa-isatool-command "\" doc"))))
    87  	(unless (string-equal docs "")
    88  	  (mapcan
    89  	   (function (lambda (docdes)