From e9ceb4ed1cce78569abb3e4792f91c7fb3a483be Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Wed, 12 Jun 2002 23:30:29 +0000 Subject: Revised find-and-forget function, which also works for count-undos. --- coq/coq.el | 102 ++++++++++++++++++++++++++++++++++++++++++++----------------- 1 file changed, 74 insertions(+), 28 deletions(-) diff --git a/coq/coq.el b/coq/coq.el index a3e5507b..194a572d 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -113,6 +113,7 @@ (defvar coq-shell-outline-regexp coq-goal-regexp) (defvar coq-shell-outline-heading-end-regexp coq-goal-regexp) +;; 3.4: no longer use generic kill-goal-command setting (defconst coq-kill-goal-command "Abort.") (defconst coq-forget-id-command "Reset %s.") (defconst coq-back-n-command "Back %s. ") ; Pierre: added @@ -167,29 +168,50 @@ ;; ;; FIXME Papageno 05/1999: must take sections in account. ;; + +;; +;; FIXME da: combine count-undos and find-and-forget, they're +;; the same now we deal with nested proofs. +;; (defun coq-count-undos (span) "Count number of undos in a span, return the command needed to undo that far." - (let ((ct 0) str i) + (let ((undos 0) (backs 0) str i) (if (and span (prev-span span 'type) (not (eq (span-property (prev-span span 'type) 'type) 'comment)) (coq-goal-command-p (span-property (prev-span span 'type) 'cmd))) + ;; FIXME: da: is Restart really necessary/useful? Small + ;; efficiency gain perhaps, but this test only works in case + ;; the previous command is exaundosly a goal. If there are + ;; intervening comments, Undos are issued using code below, + ;; which still works okay I think. "Restart." (while span (setq str (span-property span 'cmd)) - (cond ((eq (span-property span 'type) 'vanilla) - (if (proof-string-match coq-undoable-tactics-regexp str) - (setq ct (+ 1 ct)))) - ((eq (span-property span 'type) 'pbp) - (cond ((proof-string-match coq-undoable-tactics-regexp str) - (setq i 0) - (while (< i (length str)) - (if (= (aref str i) proof-terminal-char) - (setq ct (+ 1 ct))) - (setq i (+ 1 i)))) - (t nil)))) + (cond + ((eq (span-property span 'type) 'vanilla) + (cond + ((proof-string-match coq-backable-commands-regexp str) + (incf backs)) + ((proof-string-match coq-undoable-tactics-regexp str) + (incf undos)))) + ((span-property span 'nestedundos) + (setq nbacks (+ 1 nbacks (span-property span 'nestedundos)))) + ((eq (span-property span 'type) 'pbp) + ;; this is dead code for Coq right now, no PBP feature in PG. + (cond ((proof-string-match coq-undoable-tactics-regexp str) + (setq i 0) + (while (< i (length str)) + (if (= (aref str i) proof-terminal-char) + (setq undos (+ 1 undos))) + (setq i (+ 1 i)))) + (t nil)))) (setq span (next-span span 'type))) - (concat "Undo " (int-to-string ct) ".")))) + (concat + (if (> undos 0) + (concat "Undo " (int-to-string undos) ". ") "") + (if (> backs 0) + (concat "Back " (int-to-string backs) ".")))))) (defconst coq-keywords-decl-defn-regexp (proof-ids-to-regexp (append coq-keywords-decl coq-keywords-defn)) @@ -216,10 +238,15 @@ ;; Pierre: May 29 2002 added a "Back n." command in order to ;; synchronize more accurately. + +;; DA: rewrote to combine behaviour with count-undos, to work with +;; nested proofs. (defun coq-find-and-forget (span) - (let (str ans (nbacks 0) answers) - (while (and span (not ans)) + ;; NB!! Ugly use of dynamic binding here: use "end" value + ;; from caller as stopping value for loop velow. + (let (str ans (nbacks 0) (nundos 0) aborts) + (while (and span (< (span-start span) end) (not ans)) (setq str (span-property span 'cmd)) (cond ((eq (span-property span 'type) 'comment)) @@ -230,13 +257,19 @@ ;; "Unnamed_thm", though! So we don't need this test: ;;(unless (eq (span-property span 'name) proof-unnamed-theorem-name) - ;; da: test using just Back since "Reset" causes loss of proof + ;; da: try using just Back since "Reset" causes loss of proof ;; state. - (setq ans t) ;; force exit ;; (format coq-forget-id-command (span-property span 'name))) (if (span-property span 'nestedundos) (setq nbacks (+ 1 nbacks (span-property span 'nestedundos))))) + ;; 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) + (setq aborts (concat coq-kill-goal-command " " aborts))) + + ;; FIXME da: should we forget sections and Definitions using + ;; Back? ((proof-string-match (concat "\\`\\(" coq-keywords-decl-defn-regexp "\\)\\s-*\\(" proof-id @@ -269,17 +302,27 @@ coq-non-backable-commands-regexp "\\)") str))) - (setq nbacks (+ nbacks 1)))) + (incf nbacks)) + + ;; Finally all other proof commands, which are undone with + ;; Undo. But only count them if they are outermost, not + ;; within an aborted goal. + ((not aborts) + (incf nundos))) (setq span (next-span span 'type))) - (if (= nbacks 0) () - (setq answers (cons (concat " Back " (int-to-string nbacks) ". ") nil))) - (if (stringp ans) (setq answers (cons ans answers))) - (if (null answers) proof-no-command (apply 'concat answers)) - )) - - + (setq ans + (concat + (if (stringp ans) ans) + aborts + (if (> nbacks 0) + (concat "Back " (int-to-string nbacks) ". ")) + (if (> nundos 0) + (concat "Undo " (int-to-string nundos) ". ")))) + (if (null ans) + proof-no-command ;; FIXME: this is an error really (assert nil) + ans))) (defvar coq-current-goal 1 @@ -526,13 +569,16 @@ This is specific to coq-mode." proof-context-command "Print All." proof-goal-command "Goal %s." proof-save-command "Save %s." - proof-find-theorems-command "Search %s." + proof-find-theorems-command "Search %s.") ;; FIXME da: Does Coq have a help or about command? ;; proof-info-command "Help" - proof-kill-goal-command coq-kill-goal-command) + +;; 3.4: this is no longer used + (setq proof-kill-goal-command coq-kill-goal-command) (setq proof-goal-command-p 'coq-goal-command-p - proof-count-undos-fn 'coq-count-undos + ;;proof-count-undos-fn 'coq-count-undos + proof-count-undos-fn 'coq-find-and-forget proof-find-and-forget-fn 'coq-find-and-forget proof-goal-hyp-fn 'coq-goal-hyp proof-state-preserving-p 'coq-state-preserving-p -- cgit v1.2.3