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.

10 files changed, 120 insertions, 45 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.
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 9703279b..1d77cb60 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1160,8 +1160,11 @@ and that variable for details."
 ;; values as well as regexps. 
 ;; FIXME: could just as easily give default value of 
 ;; proof-std-goal-command-p here, why not?
+;; Pierre: changed this to take the span as argument instead of the string,
+;; This allows coq-mode to use a 'goalcmd attribute computed by looking at
+;; coq messages when each command is sent.
 (defcustom proof-goal-command-p 'proof-generic-goal-command-p
-  "A function to test: is this really a goal command?
+  "A function to test: is this really a goal command span?
 
 This is added as a more refined addition to proof-goal-command-regexp,
 to solve the problem that Coq and some other provers can have goals which 
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 41499e31..41f691da 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1333,7 +1333,7 @@ With ARG, turn on scripting iff ARG is positive."
 	     (and (eq proof-completed-proof-behaviour 'closeany)
 		  (> proof-shell-proof-completed 0))
 	     (and (eq proof-completed-proof-behaviour 'closegoal)
-		  (funcall proof-goal-command-p cmd))))
+		  (funcall proof-goal-command-p span))))
 	(proof-done-advancing-autosave span))
 
        ;; CASE 4: A "Require" type of command is seen (Coq).
@@ -1442,7 +1442,7 @@ With ARG, turn on scripting iff ARG is positive."
 		   (proof-string-match proof-save-command-regexp cmd))
 	      (incf lev))
 	     ;; Decrement depth when a goal is hit
-	     ((funcall proof-goal-command-p cmd)
+	     ((funcall proof-goal-command-p gspan)
 	      (decf lev))
 	     ;; Remainder cases: see if command matches something we
 	     ;; should count for a global undo
@@ -1519,7 +1519,7 @@ With ARG, turn on scripting iff ARG is positive."
 	 (gspan    (if swallow span (prev-span span 'type)))
 	 (newend   (if swallow (span-end span) (span-start span)))
 	 (cmd      (span-property span 'cmd))
-	 (newgoal  (funcall proof-goal-command-p cmd))
+	 (newgoal  (funcall proof-goal-command-p span))
 	 nam hitsave dels ncmd)
     ;; Search backwards to see if we can find a previous goal
     ;; before a save or the start of the buffer.
@@ -1533,7 +1533,8 @@ With ARG, turn on scripting iff ARG is positive."
 	  ;;(eq (span-property gspan 'type) 'proverproc) ;; NB: not necess currently
 	  (and
 	   (setq ncmd (span-property gspan 'cmd))
-	   (not (funcall proof-goal-command-p (setq cmd ncmd)))
+	   (setq cmd ncmd) ; pc: is this ok?
+	   (not (funcall proof-goal-command-p gspan))
 	   (not
 	    (and proof-save-command-regexp
 		 (proof-string-match proof-save-command-regexp cmd)
@@ -1575,7 +1576,7 @@ With ARG, turn on scripting iff ARG is positive."
   ;; is that they have no natural surrounding region, so makes
   ;; it difficult to define a region for revealing again.
   ;; [ best solution would be to support clicking on ellipsis]
-  (if (funcall proof-goal-command-p (span-property span 'cmd))
+  (if (funcall proof-goal-command-p span)
 	  (incf proof-nesting-depth))
 
   (if proof-shell-proof-completed
@@ -2280,8 +2281,7 @@ Span deletion property set to flag DELETE-REGION."
 		  (or (eq (span-property span 'type) 'proof)
 		      (eq (span-property span 'type) 'comment)
 		      (eq (span-property span 'type) 'proverproc)
-		      (not (funcall proof-goal-command-p
-				    (span-property span 'cmd)))))
+		      (not (funcall proof-goal-command-p span))))
 	(setq span (prev-span span 'type)))
       span)))
 
@@ -2620,9 +2620,10 @@ assistant."
 ;; allow settings which are string or fn, so we don't need both regexp
 ;; and function hooks, and so that the other hooks can be functions too.
 
-(defun proof-generic-goal-command-p (str)
+(defun proof-generic-goal-command-p (span)
   "Is STR a goal?  Decide by matching with `proof-goal-command-regexp'."
-  (proof-string-match-safe proof-goal-command-regexp str))
+  (proof-string-match-safe proof-goal-command-regexp
+			   (or (span-property span 'cmd) "")))
 
 (defun proof-generic-state-preserving-p (cmd)
   "Is CMD state preserving?  Match on `proof-non-undoables-regexp'."
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index b42cb310..9db2a3b3 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -343,7 +343,9 @@ Does nothing if proof assistant is already running."
 	;; could add back code above for multiple shells <2> <3>, etc.
 	;; Seems hardly worth it.
 	(apply 'make-comint  (append (list proc (car prog-name-list) nil)
-				     (cdr prog-name-list))))
+				     (cdr prog-name-list)))
+	;(message (append (list proc (car prog-name-list) nil) (cdr prog-name-list)))
+	)
 
       (setq proof-shell-buffer (get-buffer (concat "*" proc "*")))
 
diff --git a/isa/isa.el b/isa/isa.el
index 32ec46fb..22b68642 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -508,8 +508,7 @@ you will be asked to retract the file or process the remainder of it."
        (ct 0) str i)
     (if (and span (prev-span span 'type)
 	     (not (eq (span-property (prev-span span 'type) 'type) 'comment))
-	     (isa-goal-command-p
-	      (span-property (prev-span span 'type) 'cmd)))
+	     (isa-goal-command-p (prev-span span 'type)))
 	(concat "choplev 0" proof-terminal-string)
       (while span
 	(setq str (span-property span 'cmd))
@@ -531,9 +530,10 @@ you will be asked to retract the file or process the remainder of it."
       (concat "ProofGeneral.repeat_undo " 
 	      (int-to-string ct) proof-terminal-string))))
 
-(defun isa-goal-command-p (str)
+(defun isa-goal-command-p (span)
   "Decide whether argument is a goal or not"
-  (proof-string-match isa-goal-command-regexp str)) ; this regexp defined in isa-syntax.el
+  (proof-string-match isa-goal-command-regexp  ; this regexp defined in isa-syntax.el
+		      (or (span-property span 'cmd) ""))) 
 
 ;; Isabelle has no concept of a Linear context, so forgetting back
 ;; to the declaration of a particular something makes no real
diff --git a/isar/isar.el b/isar/isar.el
index 41871478..9bd0ef69 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -479,9 +479,10 @@ proof-shell-retract-files-regexp."
 
 
 
-(defun isar-goal-command-p (str)
+(defun isar-goal-command-p (span)
   "Decide whether argument is a goal or not"
-  (proof-string-match isar-goal-command-regexp str))
+  (proof-string-match isar-goal-command-regexp 
+		      (or (span-property span 'cmd) "")))
 
 (defun isar-global-save-command-p (span str)
   "Decide whether argument really is a global save command"
diff --git a/lego/lego.el b/lego/lego.el
index 1a6c10dd..e2f755ea 100644
--- a/lego/lego.el
+++ b/lego/lego.el
@@ -197,7 +197,8 @@ Given is the first SPAN which needs to be undone."
 
 (defun lego-goal-command-p (str)
   "Decide whether argument is a goal or not"
-  (proof-string-match lego-goal-command-regexp str))
+  (proof-string-match lego-goal-command-regexp
+		      (or (span-property span 'cmd) "")))
 
 (defun lego-find-and-forget (span) 
   (let (str ans)
diff --git a/plastic/plastic.el b/plastic/plastic.el
index 33b7179f..e6bf14d4 100644
--- a/plastic/plastic.el
+++ b/plastic/plastic.el
@@ -233,9 +233,10 @@ Given is the first SPAN which needs to be undone."
       (setq span (next-span span 'type)))
     (concat plastic-lit-string " &S Undo x" (int-to-string ct) proof-terminal-string)))
 
-(defun plastic-goal-command-p (str)
+(defun plastic-goal-command-p (span)
   "Decide whether argument is a goal or not"			;; NEED CHG.
-  (proof-string-match plastic-goal-command-regexp str))
+  (proof-string-match plastic-goal-command-regexp 
+		      (or (span-property span 'cmd) "")))
 
 (defun plastic-find-and-forget (span) 
 	;; count the number of spans to undo.