From 8ba99b2013e0f62c9117fc79364630ff1fbec585 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Wed, 26 Apr 2006 22:31:52 +0000 Subject: Changed the type of proof-goal-command-p. It takes now a span, which allows using a span attribute to detect goal commands. I think I modified all modes accordingly. --- lego/lego.el | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'lego') diff --git a/lego/lego.el b/lego/lego.el index 1a6c10dd..e2f755ea 100644 --- a/lego/lego.el +++ b/lego/lego.el @@ -197,7 +197,8 @@ Given is the first SPAN which needs to be undone." (defun lego-goal-command-p (str) "Decide whether argument is a goal or not" - (proof-string-match lego-goal-command-regexp str)) + (proof-string-match lego-goal-command-regexp + (or (span-property span 'cmd) ""))) (defun lego-find-and-forget (span) (let (str ans) -- cgit v1.2.3