Added a function to inspect the prompt of Coq, in order to know if we

are in proof-mode. Redundant with proof-nesting-depth.

2 files changed, 19 insertions, 0 deletions

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index b5993547..6615e584 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -106,6 +106,8 @@ Print and Check commands, put the following line in your .emacs:
 "Cd"
 "Check"
 "DelPath"
+"Define"
+"Qed"
 "End"
 "End\\s-+Silent"
 "Eval"
@@ -135,6 +137,7 @@ Print and Check commands, put the following line in your .emacs:
 "Show\\s-+Proof"
 "Show\\s-+Script"
 "Show"
+"Save"
 "Unfocus" ; ???
 )
 			 coq-user-non-backable-commands
diff --git a/coq/coq.el b/coq/coq.el
index 3b6c8f30..97c8ebb4 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -230,6 +230,22 @@
        (not (proof-string-match "Lemma.*:=" str))))
 ;; ))
 
+
+; Pierre: This is a try, for use in find-and-forget. It seems to work but 
+; is it correct with respect to the asynchronous communication between Coq 
+; and emacs? 
+; FIXME: Pierre The prompt should be (is?) available by something cleaner
+; than this ugly buffer switching. David? :-)
+(defun coq-proof-mode-p ()
+  "Look at the last line of the *coq* buffer to see if the prompt 
+is the toplevel \"Coq <\". Returns nil if yes. Allows to know if we
+are currentlly in proof mode. This assumes that no \"Resume\" Command
+have been used."
+  (save-window-excursion 
+	 (switch-to-buffer "*coq*")
+	 (not (string-match "^Coq < " (buffer-substring (- (point-max) 8) (point-max))))))
+
+
 ;; TODO : add the stuff to handle the "Correctness" command 
 
 ;; Pierre: May 29 2002 added a "Back n. " command in order to