From 2997c618372cca7b2d572b02dc393791d54fdb7c Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Tue, 18 Jun 2002 18:19:29 +0000 Subject: Test using proof-nesting-depth before calling Reset --- coq/coq.el | 20 +++++++++++--------- 1 file changed, 11 insertions(+), 9 deletions(-) diff --git a/coq/coq.el b/coq/coq.el index 192763cf..718551a6 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -260,20 +260,23 @@ ;; 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))) + (setq aborts (concat coq-kill-goal-command " " aborts)) + (setq proof-nesting-depth (min 0 (1- proof-nesting-depth)))) ;; FIXME da: should we forget sections and Definitions using ;; Back? - ((proof-string-match - (concat "\\`\\(" coq-keywords-decl-defn-regexp "\\)\\s-*\\(" - proof-id - ;; Section .. End Section should be atomic! - "\\)\\s-*[\\[,:.]") str) + ((and + (eq proof-nesting-depth 0) + (proof-string-match + (concat "\\`\\(" coq-keywords-decl-defn-regexp "\\)\\s-*\\(" + proof-id + ;; Section .. End Section should be atomic! + "\\)\\s-*[\\[,:.]") str)) (setq ans (format coq-forget-id-command (match-string 2 str)))) ;; If it's not a goal but it contains "Definition" then it's a - ;; declaration - ((and (not (coq-goal-command-p str)) + ;; declaration [ da: is this not covered by above case??? ] + ((and (eq proof-nesting-depth 0) (proof-string-match (concat "Definition\\s-+\\(" proof-id "\\)\\s-*") str)) (setq ans (format coq-forget-id-command (match-string 2 str)))) @@ -286,7 +289,6 @@ ;; definable elisp variables coq-user... to avoid this problem ;; anyway. ((and - (not (coq-goal-command-p str)) ;; unsaved goals ;; now we should match all things that do not deal with Back (not (proof-string-match (concat "\\`\\(" coq-tactics-regexp "\\)") -- cgit v1.2.3