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.
---
 plastic/plastic.el | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'plastic')

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.
-- 
cgit v1.2.3