Changed the type of proof-goal-command-p. It takes now a span, which

allows using a span attribute to detect goal commands.

I think I modified all modes accordingly.

3 files changed, 91 insertions, 25 deletions

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 360ab3ac..349f5b86 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -90,6 +90,8 @@ version of coq by doing 'coqtop -v'." )
     "CoInductive"
 	 "Definition" ;; careful: if not followed by :=, then it is a goal cmd
     "Fixpoint"
+    "GenFixpoint" ;; careful: may or not be a proof start
+    "Function"  ;; careful: may or not be a proof start
     "CoInductive"
     "Inductive"
     "Inductive\\s-+Set"
@@ -107,12 +109,14 @@ version of coq by doing 'coqtop -v'." )
 (defvar coq-keywords-goal
   '("Add\\s-+Morphism"
 	 "Chapter"
-	 "Declare\\s-+Module";;only if not followed by:=(see coq-proof-mode-p in coq.el)
+	 "Declare\\s-+Module";;only if not followed by:=(see coq-goal-command-p below)
 	 "Module"
 	 "Module\\s-+Type"
 	 "Section"
 	 "Correctness"
-	 "Definition";; only if not followed by := (see coq-proof-mode-p in coq.el)
+	 "Definition";; only if not followed by := (see coq-goal-command-p below)
+	 "GenFixpoint" ;;if {measure} or {wf} (see coq-goal-command-p below)
+	 "Function" ;;if {measure} or {wf} (see coq-goal-command-p below)
 	 "Fact"
 	 "Goal"
 	 "Lemma"
@@ -127,6 +131,10 @@ version of coq by doing 'coqtop -v'." )
 ;; Future improvement may simply to be allow a function value for
 ;; proof-goal-regexp.
 
+;; FIXME Pierre: the right way IMHO here would be to set a span
+;; property 'goalcommand when coq prompt says it (if the name of
+;; current proof has changed).
+
 ;; excerpt of Jacek Chrzaszcz, implementer of the module system: sorry
 ;; for the french:
 ;*) suivant les suggestions de Chritine, pas de mode preuve dans un type de
@@ -157,32 +165,71 @@ of STRG matching REGEXP. Empty match are counted once."
         (setq str (substring str (match-end 0)))))
     nbmatch))
 
-
-
-(defun coq-goal-command-p (str)
-  "Decide whether argument is a goal or not"
+; This function is used for amalgamating a proof into a single
+; goal-save region (proof-goal-command-p used in
+; proof-done-advancing-save in generic/proof-script.el). It is the
+; test when looking backward the start of the proof.  It is NOT used
+; elsewhere in the backtrack mechanism of coq > v8.1
+; (coq-find-and-forget in coq.el uses state numbers, proof numbers and
+; lemma names given in the prompt)
+
+; compatibility with v8.0, will delete it some day
+(defun coq-goal-command-p-v80 (str)
+  "See `coq-goal-command-p'."
   (let* ((match (coq-count-match "\\<match\\>" str))
-		  (with (coq-count-match "\\<with\\>" str))
-		  (letwith (+ (coq-count-match "\\<let\\>" str) (- with match)))
-		  (affect (coq-count-match ":=" str)))
+	 (with (coq-count-match "\\<with\\>" str))
+	 (letwith (+ (coq-count-match "\\<let\\>" str) (- with match)))
+	 (affect (coq-count-match ":=" str)))
 		  
-	 (and (proof-string-match coq-goal-command-regexp str)
-			(not									 ; 
-			 (and 
-			  (proof-string-match "\\`\\(Local\\|Definition\\|Lemma\\|Module\\)\\>" str)
-			  (not (= letwith affect))))
-			(not (proof-string-match "\\`Declare\\s-+Module\\(\\w\\|\\s-\\|<\\)*:" str))
-			)
+    (and (proof-string-match coq-goal-command-regexp str)
+	 (not				; 
+	  (and 
+	   (proof-string-match "\\`\\(Local\\|Definition\\|Lemma\\|Module\\)\\>" str)
+	   (not (= letwith affect))))
+	 (not (proof-string-match "\\`Declare\\s-+Module\\(\\w\\|\\s-\\|<\\)*:" str))
 	 )
+    )
   )
 
+;We use this function in order to detect [Declare] modules [Type]
+;openings. goal openings are detected by parsing the prompt.
+
+(defun coq-goal-command-str-v81-p (str)
+  "Decide whether STR is a module opening or not. 
+Used by `coq-goal-command-p'"
+  (let* ((match (coq-count-match "\\<match\\>" str))
+	 (with (coq-count-match "\\<with\\>" str))
+	 (letwith (+ (coq-count-match "\\<let\\>" str) (- with match)))
+	 (affect (coq-count-match ":=" str)))
+    (and (proof-string-match "\\`\\(Module\\)\\>" str)
+	 (= letwith affect))
+	 ))
+
+
+;; TODO: have something in the prompt telling the name of all opened
+;; modules (like for open goals), and use it to set goalcmd --> no more
+;; need to look at "Modules" --> no more need to coq-goal-command-str-v81-p
+(defun coq-goal-command-p-v81 (span)
+  "see `coq-goal-command-p'"
+  (or (span-property span 'goalcmd)
+      ;; module starts are detected here
+      (coq-goal-command-str-v81-p (or (span-property span 'cmd) ""))))
+
+
+(defun coq-goal-command-p (span)
+  "Decide whether argument is a goal or not."
+ (cond 
+  (coq-version-is-V8-1 (coq-goal-command-p-v81 span))
+  (coq-version-is-V8-0 (coq-goal-command-p-v80 span))
+  (t (coq-goal-command-p-v80 span)) ;; this is temporary
+  ))
 
 (defvar coq-keywords-save-strict
   '("Defined"
     "Save"
     "Qed"
     "End"
-	 "Admitted"
+    "Admitted"
 	 ))
 
 (defvar coq-keywords-save
@@ -197,6 +244,7 @@ of STRG matching REGEXP. Empty match are counted once."
 		)
   )
 
+
 (defvar coq-keywords-kill-goal 
   '("Abort"))
 
diff --git a/coq/coq.el b/coq/coq.el
index 10fd3e66..31875623 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -323,7 +323,6 @@ toplevel \"Coq <\".  Returns nil if yes.  This assumes that no
          (s (string-match regex lastprompt))
          (lprf (match-string 3 lastprompt))
          )
-    (message lprf)
     (cons (string-to-int (match-string 2 lastprompt))
           (cons (string-to-int (match-string 4 lastprompt))
                 (cons (build-list-id-from-string lprf) nil)))
@@ -367,6 +366,16 @@ pending proofs (in a list)."
   (set-span-property span 'statenum val)
   )
 
+(defun coq-get-span-goalcmd (span)
+  "Return the 'goalcmd flag of the SPAN."
+  (span-property span 'goalcmd)
+  )
+
+(defun coq-set-span-goalcmd (span val)
+  "Set the 'goalcmd flag of the SPAN to VAL."
+  (set-span-property span 'goalcmd val)
+  )
+
 (defun coq-set-span-proofnum (span val)
   "Set the proof number of the SPAN to VAL."
   (set-span-property span 'proofnum val)
@@ -398,12 +407,21 @@ This number is in the *last but one* prompt (variable `coq-last-but-one-statenum
 If locked span already has a state number, thne do nothing. Also updates
 `coq-last-but-one-statenum' to the last state number for next time."
   (if (and proof-shell-last-prompt proof-script-buffer)
+      ;; infos = promt infos of the very last prompt
+      ;; sp = last locked span, which we want to fill with prompt infos
       (let ((sp    (proof-last-locked-span))
             (infos (or (coq-last-prompt-info-safe) '(0 0 nil)))
             )
         (unless (or (not sp) (coq-get-span-statenum sp))
           (coq-set-span-statenum sp coq-last-but-one-statenum))
         (setq coq-last-but-one-statenum (car infos))
+        ;; set goalcmd property if this is a goal start 
+        ;; (ie proofstack has changed and not a save cmd)
+        (unless 
+            (or (not sp) (equal (span-property sp 'type) 'goalsave)
+                (<= (length (car (cdr (cdr infos))))
+                    (length coq-last-but-one-proofstack)))
+          (coq-set-span-goalcmd sp t))
         ;; testing proofstack=nil is not good here because nil is the empty list OR
         ;; the no value, so we test proofnum as it is always set at the same time.
         ;; This is why this test is done before the next one (which sets proofnum)
diff --git a/coq/ex-module.v b/coq/ex-module.v
index 5b9d638a..413a4966 100644
--- a/coq/ex-module.v
+++ b/coq/ex-module.v
@@ -28,6 +28,10 @@ Module M.
     Parameter T:Set.
     Parameter x:T.
   End SIG.
+  Module Type SIG'.
+    Parameter T:Set.
+    Parameter x:T.
+  End SIG'.
   Lemma toto : O=O.
     Definition t:=nat.
     trivial.
@@ -66,16 +70,13 @@ Module Type N'.
   Module Type M'.
     Declare Module K:N.SIG.
   End M'.
-  Declare Module N''.
+(*   Declare Module N''. *)
     Definition T:=nat.
     Definition x:=O.
-  End N''.
+(*   End N''. *)
   
   Declare Module N':M.SIG. (* no interactive def started *)
-  Declare Module N''':= N'. (* no interactive def started *)
-  Declare Module N''''. (* interactive def started *)
-	 Parameter foo:nat.
-  End N''''.            (* interactive def ended *)
+  Declare Module N''' :M.SIG. (* no interactive def started *)
 End N'.
 
     
@@ -90,7 +91,6 @@ Save.
     
 Lemma bar:O=O.
   Module Type L. (* This should not be allowed by Coq, since the End L. below fails *)
-	 Axiom foo: O=O.
   End L. (* fails --> if we go back to Module Type: unsync *)
   Module I.
 End I.