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 /plastic | |
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 'plastic')
-rw-r--r-- | plastic/plastic.el | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/plastic/plastic.el b/plastic/plastic.el index 33b7179f..e6bf14d4 100644 --- a/plastic/plastic.el +++ b/plastic/plastic.el @@ -233,9 +233,10 @@ Given is the first SPAN which needs to be undone." (setq span (next-span span 'type))) (concat plastic-lit-string " &S Undo x" (int-to-string ct) proof-terminal-string))) -(defun plastic-goal-command-p (str) +(defun plastic-goal-command-p (span) "Decide whether argument is a goal or not" ;; NEED CHG. - (proof-string-match plastic-goal-command-regexp str)) + (proof-string-match plastic-goal-command-regexp + (or (span-property span 'cmd) ""))) (defun plastic-find-and-forget (span) ;; count the number of spans to undo. |