aboutsummaryrefslogtreecommitdiffhomepage
path: root/plastic/plastic.el
diff options
context:
space:
mode:
Diffstat (limited to 'plastic/plastic.el')
-rw-r--r--plastic/plastic.el5
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.