aboutsummaryrefslogtreecommitdiffhomepage
path: root/af2
diff options
context:
space:
mode:
authorGravatar Christophe Raffalli <christophe.raffalli@univ-savoie.fr>2000-09-18 16:39:35 +0000
committerGravatar Christophe Raffalli <christophe.raffalli@univ-savoie.fr>2000-09-18 16:39:35 +0000
commit0cc60b96f6f249f3b2637ace6abc1c6f9d6c3181 (patch)
treed5d4bc0bcea4e8e4c6006e70e467989227f0612d /af2
parentffe0fb867dd09e100f453118f58e8e510f216409 (diff)
*** empty log message ***
Diffstat (limited to 'af2')
-rw-r--r--af2/af2-fun.el6
1 files changed, 4 insertions, 2 deletions
diff --git a/af2/af2-fun.el b/af2/af2-fun.el
index 8e253232..5da642a3 100644
--- a/af2/af2-fun.el
+++ b/af2/af2-fun.el
@@ -31,9 +31,10 @@ send a compile command to af2 for the theorem which name is under the cursor."
)
(defun af2-find-and-forget (span)
- (let (str ans tmp)
- (while span
+ (let (str ans tmp (lsp -1))
+ (while span
(setq str (proof-remove-comment (span-property span 'cmd)))
+
(cond
((eq (span-property span 'type) 'comment))
@@ -52,6 +53,7 @@ send a compile command to af2 for the theorem which name is under the cursor."
(match-string 2 str)) ans))))
+ (setq lsp (span-start span))
(setq span (next-span span 'type)))
(or ans proof-no-command)))