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

4 files changed, 111 insertions, 9 deletions

diff --git a/coq/coq.el b/coq/coq.el
index 6ca92951..bc4667e2 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -5,6 +5,12 @@
 
 ;; $Id$ 
 
+;TODO Papageno 05/1999:
+;
+;* Correct the C-c C-c bug
+;* Fix the coq-lift-global code
+;* color of error messages is beuark
+
 (require 'proof-script)
 (require 'coq-syntax)
 
@@ -24,7 +30,13 @@
 
 (setq tags-always-exact t) ; Tags is unusable with Coq library otherwise:
 
-(defcustom coq-tags "/usr/local/lib/coq/theories/TAGS"
+(defun coq-library-directory () 
+  (let ((c (substring (shell-command-to-string "coqtop -where") 0 -1 )))
+    (if (string-match c "not found")
+	  "/usr/local/lib/coq"
+      c)))
+
+(defcustom coq-tags (concat (coq-library-directory) "/theories/TAGS")
   "the default TAGS table for the Coq library"
   :type 'string
   :group 'coq)
@@ -75,7 +87,7 @@
 
 (defvar coq-outline-regexp
   (proof-ids-to-regexp 
-	   '("Section" "Chapter" "Goal" "Lemma" "Theorem" "Fact"
+	   '("Correctness" "Section" "Chapter" "Goal" "Lemma" "Theorem" "Fact"
 	   "Remark" "Record" "Inductive" "Definition")))
 
 (defvar coq-outline-heading-end-regexp "\.\\|\\*)")
@@ -98,6 +110,13 @@
    nil
    (coq-shell-mode-config))
 
+(eval-and-compile
+  (define-derived-mode coq-response-mode proof-response-mode
+    "CoqResp" nil
+    (setq font-lock-keywords coq-font-lock-terms)
+    (coq-init-syntax-table)
+    (proof-response-config-done)))
+ 
 (define-derived-mode coq-mode proof-mode
    "coq" nil
    (coq-mode-config))
@@ -248,17 +267,23 @@
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 (defun coq-Intros () 
-  "List proof state." 
+  "Shortcut for Intros.
+
+  This is specific to coq-mode." 
   (interactive) 
   (insert "Intros "))
 
 (defun coq-Apply () 
-  "List proof state."  
+  "Shortcut for Apply
+
+  This is specific to coq-mode."  
   (interactive) 
   (insert "Apply "))
 
 (defun coq-Search ()
-  "Search for type in goals."
+  "Search for type in goals
+
+  This is specific to coq-mode."
   (interactive)
   (let (cmd)
     (proof-shell-ready-prover) ;; was (proof-check-process-available)
@@ -266,6 +291,29 @@
     (proof-shell-invisible-command
      (concat "Search " cmd proof-terminal-string))))
 
+(defun coq-begin-Section ()
+  "begins a Coq section."
+  (interactive)
+  (insert "Section "))
+
+(defun coq-end-Section ()
+  "Ends a Coq section."
+  (interactive)
+  (let ((section 
+	 (save-excursion 
+	   (progn 
+	     (setq count 1) ; The number of section already "Ended" + 1
+	     (while (and (> count 0) 
+			 (search-backward-regexp 
+			  "Chapter\\|Section\\|End" 0 t))
+	       (if (char-equal (char-after (point)) ?E)
+		   (setq count (1+ count))
+		 (setq count (1- count))))
+	     (buffer-string
+	      (progn (beginning-of-line) (point)) 
+	      (progn (end-of-line) (point)))))))
+    (insert (replace-string "Section" "End" section))))
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;   Indentation                                                    ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -314,6 +362,23 @@
 
    (t stack)))
 
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;    To guess the command line options   ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(defun coq-guess-command-line (filename)
+  "Guess the right command line options to compile FILENAME using `make -n'"
+  (let* ((dir (file-name-directory filename))
+	 (compiled-file (concat (substring 
+				 filename 0 
+				 (string-match ".v$" filename)) ".vo"))
+	 (command (shell-command-to-string 
+		   (concat  "cd " dir ";"
+			    "gmake -n -W " filename " " compiled-file
+			    "| sed s/coqc/coqtop/"))))
+    (concat 
+     (substring command 0 (string-match " [^ ]*$" command))
+     " -emacs")))
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;   Coq shell startup and exit hooks                               ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -359,6 +424,8 @@
 
   (setq proof-mode-for-script 'coq-mode)
 
+  (setq proof-guess-command-line 'coq-guess-command-line)
+
   (setq proof-prf-string "Show"
 	proof-ctxt-string "Print All"
 	proof-help-string "Help")
@@ -389,6 +456,8 @@
   (define-key (current-local-map) [(control c) ?I] 'coq-Intros)
   (define-key (current-local-map) [(control c) ?a] 'coq-Apply)
   (define-key (current-local-map) [(control c) (control s)] 'coq-Search)
+  (define-key (current-local-map) [(control c) ?s] 'coq-Section)
+  (define-key (current-local-map) [(control c) ?e] 'coq-end-Section)
 
 ;; outline
   
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 15bab2f4..76640043 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -1587,6 +1587,15 @@ If non-nil, query user which program to run for the inferior process.
 The default value is @code{nil}.
 @end defopt
 
+@c TEXI DOCSTRING MAGIC: proof-prog-name-guess
+@defopt proof-prog-name-guess
+If non-nil, ProofGeneral tries to run `make -n' to guess
+the command line arguments for the proof assistant
+(Currently implemented for Coq only)
+
+The default value is @code{nil}.
+@end defopt
+
 
 @c TEXI DOCSTRING MAGIC: proof-rsh-command
 @defopt proof-rsh-command 
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