I've added the custom option 'prog-name-guess' in the generic part and

the function coq-guess-command-line in the coq part. Every prover
should have the functon *-guess-command-line that uses, for example,
the output of "make -n" to guess the correct command line options of
the prover.

Patrick

2 files changed, 28 insertions, 4 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index ba09379c..6e8c3806 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -71,6 +71,13 @@
   :type 'boolean
   :group 'proof-general)
 
+(defcustom proof-prog-name-guess nil
+  "*If non-nil, use `proof-guess-command-line' to guess the correct
+   value of proof-prog-name when starting proof assisant
+   This option is compatible with proof-prog-name-ask"
+  :type 'boolean
+  :group 'proof-general)
+
 (and (featurep 'toolbar)
 (defcustom proof-toolbar-inhibit nil
   "*Non-nil prevents toolbar being used for script buffers."
@@ -384,6 +391,12 @@ Suggestion: this can be set in the script mode configuration."
   :type 'function
   :group 'prover-config)
 
+(defcustom proof-guess-command-line nil
+  "Function that takes a filename as argument, runs `make -n' and 
+  translates the result into an invocation of the proof assistant
+  with the same command line options"
+  :type 'function
+  :group 'prover-config)
 
 
 
@@ -1032,7 +1045,6 @@ See documentation of proof-shell-start-char."
   :group 'proof-goals)
 
 
-
 
 ;;
 ;; 7. Splash screen settings
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 46cb5cd4..9260e03e 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -195,6 +195,17 @@ Does nothing if proof assistant is already running."
       ()
     (run-hooks 'proof-pre-shell-start-hook)
     (setq proof-included-files-list nil)
+
+    ;; Added 05/99 by Papageno
+    (let ((name (buffer-file-name (current-buffer))))
+      ;; FIXME : we check that the buffer corresponds to a file,
+      ;; but we do not check that it is in coq- or isa-mode
+      (if (and name proof-prog-name-guess proof-guess-command-line)
+	  (let ((dir (file-name-directory name)))
+	    (if (file-exists-p (concat dir "Makefile"))
+		(setq proof-prog-name 
+		      (apply proof-guess-command-line (list name)))))))
+
     (if proof-prog-name-ask
 	(save-excursion
 	  (setq proof-prog-name (read-shell-command "Run process: "
@@ -205,14 +216,15 @@ Does nothing if proof assistant is already running."
     (let ((proc
 	   (concat "Inferior "
 		   (substring proof-prog-name
-			      (string-match "[^/]*$" proof-prog-name)))))
+			       (string-match "[^ /]* " proof-prog-name)
+			       (string-match  " " proof-prog-name)))))
       (while (get-buffer (concat "*" proc "*"))
 	(if (string= (substring proc -1) ">")
 	    (aset proc (- (length proc) 2) 
 		  (+ 1 (aref proc (- (length proc) 2))))
 	  (setq proc (concat proc "<2>"))))
-
-      (message (format "Starting %s process..." proc))
+      
+      (message (format "Starting process : %s" proof-prog-name))
 
       ;; Starting the inferior process (asynchronous)
       (let ((prog-name-list