From 2bf4a7f0b3cf660c6b215a3e49d80115409e192e Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Tue, 28 Aug 2001 15:53:17 +0000 Subject: Change of proof span type back to goalsave --- coq/coq.el | 2 +- isar/isar.el | 2 +- lego/lego.el | 2 +- phox/phox-fun.el | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/coq/coq.el b/coq/coq.el index 6e2325f1..be65c1cd 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -203,7 +203,7 @@ ((eq (span-property span 'type) 'comment)) - ((eq (span-property span 'type) 'proof) + ((eq (span-property span 'type) 'goalsave) ;; Note da 6.10.99: in Lego and Isabelle, it's trivial to ;; forget an unnamed theorem. Coq really does use the ;; identifier "Unnamed_thm", though! So we don't need diff --git a/isar/isar.el b/isar/isar.el index d1a27bec..ba8d4469 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -371,7 +371,7 @@ proof-shell-retract-files-regexp." ((or (eq (span-property span 'type) 'comment) (proof-string-match isar-undo-skip-regexp str))) ;; finished goal: undo - ((eq (span-property span 'type) 'proof) + ((eq (span-property span 'type) 'goalsave) (setq ans isar-undo)) ;; open goal: skip and exit ((proof-string-match isar-goal-command-regexp str) diff --git a/lego/lego.el b/lego/lego.el index 087b775a..ea49805f 100644 --- a/lego/lego.el +++ b/lego/lego.el @@ -207,7 +207,7 @@ Given is the first SPAN which needs to be undone." ((eq (span-property span 'type) 'comment)) - ((eq (span-property span 'type) 'proof) + ((eq (span-property span 'type) 'goalsave) (unless (eq (span-property span 'name) proof-unnamed-theorem-name) (setq ans (format lego-forget-id-command (span-property span 'name))))) ;; alternative definitions diff --git a/phox/phox-fun.el b/phox/phox-fun.el index 22d3e717..7592a87e 100644 --- a/phox/phox-fun.el +++ b/phox/phox-fun.el @@ -173,7 +173,7 @@ or for optional argument TABLE." ((eq (span-property span 'type) 'comment)) - ((eq (span-property span 'type) 'proof) + ((eq (span-property span 'type) 'goalsave) (if (proof-string-match phox-prove-claim-regexp str) (setq ans (concat (format phox-forget-proof-command (match-string 4 str)) ans)) -- cgit v1.2.3