diff options
| author | Pierre Courtieu | 2006-07-20 08:30:34 +0000 |
|---|---|---|
| committer | Pierre Courtieu | 2006-07-20 08:30:34 +0000 |
| commit | 67b217606f87cb13be362982c2ec7f996f7a281d (patch) | |
| tree | 054c2c1608b02e38c7cf144ce4f9f054b0153010 | |
| parent | ceb90ae8673b7a7989c8049000e4ec95cf727667 (diff) | |
fixed a bug with scripting with coq v8.0.
| -rw-r--r-- | coq/coq-syntax.el | 19 | ||||
| -rw-r--r-- | coq/coq.el | 2 |
2 files changed, 17 insertions, 4 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 5eba1e77..c3402ecb 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -174,7 +174,7 @@ of STRG matching REGEXP. Empty match are counted once." ; lemma names given in the prompt) ; compatibility with v8.0, will delete it some day -(defun coq-goal-command-p-v80 (str) +(defun coq-goal-command-str-v80-p (str) "See `coq-goal-command-p'." (let* ((match (coq-count-match "\\<match\\>" str)) (with (coq-count-match "\\<with\\>" str)) @@ -212,6 +212,11 @@ Used by `coq-goal-command-p'" (proof-string-match "\\`\\(Section\\|Chapter\\)\\>" str)) +(defun coq-goal-command-str-v81-p (str) + "Decide syntactically whether STR is a goal start or not. Use + `coq-goal-command-p-v81' on a span instead if posible." + (coq-goal-command-str-v80-p str) + ) ;; This is the function that tests if a SPAN is a goal start. All it ;; has to do is look at the 'goalcmd attribute of the span. @@ -231,13 +236,21 @@ Used by `coq-goal-command-p'" (coq-module-opening-p str)) ))) +(defun coq-goal-command-str-p (str) + "Decide whether argument is a goal or not. Use + `coq-goal-command-p' on a span instead if posible." + (cond + (coq-version-is-V8-1 (coq-goal-command-str-v81-p str)) + (coq-version-is-V8-0 (coq-goal-command-str-v80-p str)) + (t (coq-goal-command-p-str-v80 str)) ;; this is temporary + )) (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-property span 'cmd))) - (t (coq-goal-command-p-v80 (span-property span 'cmd))) ;; this is temporary + (coq-version-is-V8-0 (coq-goal-command-str-v80-p (span-property span 'cmd))) + (t (coq-goal-command-str-v80-p (span-property span 'cmd))) ;; this is temporary )) (defvar coq-keywords-save-strict @@ -530,7 +530,7 @@ If locked span already has a state number, thne do nothing. Also updates ;; Unsaved goal commands: each time we hit one of these ;; we need to issue Abort to drop the proof state. - ((coq-goal-command-p str) (incf naborts)) ; FIX: nundos<-0 ? + ((coq-goal-command-str-p str) (incf naborts)) ; FIX: nundos<-0 ? ;; If we are already outside a proof, issue a Reset. [ improvement would be ;; to see if the undoing will take us outside a proof, and use the first Reset |