diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2006-04-26 22:31:52 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2006-04-26 22:31:52 +0000 |
| commit | 8ba99b2013e0f62c9117fc79364630ff1fbec585 (patch) | |
| tree | 1ecc9083150779a527fab764508ac9dab7d78096 /lego | |
| parent | fc774de804417a399094f61de1880e75b556c851 (diff) | |
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.
Diffstat (limited to 'lego')
| -rw-r--r-- | lego/lego.el | 3 |
1 files changed, 2 insertions, 1 deletions
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) |