--- 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)