Add <PA>-prog-args and <PA>-prog-env

2 files changed, 48 insertions, 29 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index fb8218db..e4f32d62 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -6,7 +6,7 @@
 ;;
 ;; Maintainer:  Proof General maintainer <da+pg-feedback@inf.ed.ac.uk>
 ;;
-;; $Id$
+;; proof-config.el,v 8.10 2005/09/14 19:11:42 makarius Exp
 ;;
 ;; This file declares all user options and prover-specific
 ;; configuration variables for Proof General.  The variables
@@ -387,7 +387,7 @@ set to a space."
   :type 'string
   :group 'proof-user-options)
 
-(defcustom proof-rsh-command ""
+(defcustom proof-rsh-command nil
   "*Shell command prefix to run a command on a remote host.  
 For example,
 
@@ -400,7 +400,7 @@ The protocol used should be configured so that no user interaction
 (passwords, or whatever) is required to get going.  For proper
 behaviour with interrupts, the program should also communicate
 signals to the remote host."
-  :type 'string
+  :type '(choice string nil)
   :group 'proof-user-options)
 
 (defcustom proof-disappearing-proofs nil
@@ -447,7 +447,7 @@ signals to the remote host."
 		     (list (list (list 'type ty) '(class color)
 				 (list 'background 'dark))
 			   (quote ,bd))))
-     '(x mswindows gtk mac)))
+     '(x mswindows gtk)))
     (list (list t (quote ,ow)))))
 
 (defface proof-queue-face 
@@ -739,9 +739,8 @@ If a function, it should return the command string to insert."
     (interrupt  "Interrupt Prover"    "Interrupt the proof assistant (warning: may break synchronization)" t)
     (restart	"Restart Scripting"   "Restart scripting (clear all locked regions)" t)
     (visibility "Toggle Visibility"   nil t)
-; PG 3.6: remove Info item from toolbar; it's not very useful and under PA->Help anyway
-;    (info	nil		      "Show online proof assistant information" t
-;				      proof-info-command)
+    (info	nil		      "Show online proof assistant information" t
+				      proof-info-command)
     (help	nil		      "Proof General manual" t))
 "Example value for proof-toolbar-entries.  Also used to define scripting menu.
 This gives a bare toolbar that works for any prover, providing the
@@ -1508,6 +1507,7 @@ See pg-user.el: pg-create-in-span-context-menu for more hints."
 
 (defcustom proof-prog-name nil
   "System command to run the proof assistant in the proof shell.
+May contain arguments separated by spaces, but see also `proof-prog-args'.
 Suggestion: this can be set in proof-pre-shell-start-hook from
 a variable which is in the proof assistant's customization
 group.  This allows different proof assistants to coexist
@@ -1515,6 +1515,21 @@ group.  This allows different proof assistants to coexist
   :type 'string
   :group 'proof-shell)
 
+(defpgcustom prog-args nil
+  "Arguments to be passed to `proof-prog-name' to run the proof assistant.
+If non-nil, will be treated as a list of arguments for `proof-prog-name'.
+Otherwise `proof-prog-name' will be split on spaces to form arguments."
+  :type '(list string)
+  :group 'proof-shell)
+
+(defpgcustom prog-env nil
+  "Modifications to `process-environment' made before running `proof-prog-name'.
+Each element should be a string of the form ENVVARNAME=VALUE.
+They will be added to the environment before launching the prover (but
+not pervasively)"
+  :type '(list string)
+  :group 'proof-shell)
+
 (defcustom proof-shell-auto-terminate-commands t
   "Non-nil if Proof General should try to add terminator to every command.
 If non-nil, whenever a command is sent to the prover using
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index acb70b7e..c86c9dea 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -5,7 +5,7 @@
 ;;            Thomas Kleymann and Dilip Sequeira
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
-;; $Id$
+;; proof-shell.el,v 8.15 2005/09/30 09:45:36 da Exp
 ;;
 
 (require 'proof-menu)
@@ -285,20 +285,21 @@ Does nothing if proof assistant is already running."
       (message "Starting process: %s" proof-prog-name)
 
       ;; Starting the inferior process (asynchronous)
-      (let ((prog-name-list
-	     (proof-string-to-list
-	      ;; Cut in proof-rsh-command if it's non-nil and
-	      ;; non whitespace.  FIXME: whitespace at start
-	      ;; of this string is nasty.
+      (let* ((prog-name-list1
+	      (if (proof-ass prog-args)
+		 ;; If argument list supplied in <PA>-prog-args, use that.
+		  (cons proof-prog-name (proof-ass prog-args))
+		;; Otherwise, cut prog name on spaces (FIXME: could be whitespace?)
+		(proof-string-to-list proof-prog-name " ")))
+	     (prog-name-list
+		;; Cut in proof-rsh-command if it's non-nil 
 	      (if (and proof-rsh-command
-		       (not (string-match "^[ \t]*$" proof-rsh-command)))
-		  (concat proof-rsh-command " " proof-prog-name)
-		proof-prog-name)
-	      ;; Split on spaces: FIXME: maybe should be whitespace.
-	      " "))
+		       (> (length proof-rsh-command) 0))
+		  (cons proof-rsh-command prog-name-list1)
+		prog-name-list1))
 
-	    (process-connection-type
-	     proof-shell-process-connection-type)
+	     (process-connection-type
+	      proof-shell-process-connection-type)
 
 	    ;; PG 3.5: adjust the LANG variable to remove UTF-8
 	    ;; encoding that may be there.  This fix is targeted at RH
@@ -306,16 +307,19 @@ Does nothing if proof assistant is already running."
 	    ;; default.  FIXME: unfortunately this fix doesn't work;
 	    ;; it's not enough to alter process-environment to effect
 	    ;; a locale change.  In bash, LANG=x <prog> works though.
+	    ;; PG 3.6: allow other adjustments to environments from
+	    ;; <PA>-prog-env
 	    (process-environment
-	     (if proof-shell-unicode           ;; if specials not used,
-		 process-environment	       ;; leave it alone
-	       (cons
-		(if (getenv "LANG")
-		    (format "LANG=%s"
-			    (replace-in-string (getenv "LANG")
-					       "\\.UTF-8" ""))
-		  "LANG=C")
-		process-environment)))
+	     (append (proof-ass prog-env)
+		     (if proof-shell-unicode           ;; if specials not used,
+			 process-environment	       ;; leave it alone
+		       (cons
+			(if (getenv "LANG")
+			    (format "LANG=%s"
+				    (replace-in-string (getenv "LANG")
+						       "\\.UTF-8" ""))
+			  "LANG=C")
+			process-environment))))
 
 	    ;; Since we use codes between 128 and 255 as special, we want to
 	    ;; treat the output of the process as binary, except for