From 9c77766565cc9c29289ecf1c7d6c964d6af388ce Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
Date: Thu, 5 Jun 2003 10:45:12 +0000
Subject: Make find-and-forget robust for proverproc regions

---
 coq/coq.el         | 5 +++--
 isar/isar.el       | 1 +
 lego/lego.el       | 2 ++
 phox/phox-fun.el   | 4 +++-
 plastic/plastic.el | 1 +
 5 files changed, 10 insertions(+), 3 deletions(-)

diff --git a/coq/coq.el b/coq/coq.el
index 810db4b4..2476fbf4 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -267,7 +267,8 @@ toplevel \"Coq <\". Returns nil if yes. This assumes that no
 ;; nested proofs.
 
 
-(defun coq-is-comment-p (span) (eq (span-property span 'type) 'comment))
+(defun coq-is-comment-or-proverprocp (span) 
+  (memq (span-property span 'type) '(comment proverproc)))
 (defun coq-is-goalsave-p (span) (eq (span-property span 'type) 'goalsave))
 (defun coq-is-module-equal-p (str) ;;cannot appear vith coq < 7.4
   (and (proof-string-match "\\`\\(Declare\\s-\\)?\\s-*\\<Module\\>.*:=" str)
@@ -304,7 +305,7 @@ toplevel \"Coq <\". Returns nil if yes. This assumes that no
     (while (and span (not ans))
       (setq str (span-property span 'cmd))
       (cond
-       ((coq-is-comment-p span)) ; do nothing
+       ((coq-is-comment-or-proverprocp span)) ; do nothing
 
        ;; Module <Type> T ... :=... . inside proof ->  like Definition...:=...  
        ;; (should actually be disallowed in coq)
diff --git a/isar/isar.el b/isar/isar.el
index 92ad071b..8b0d8327 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -423,6 +423,7 @@ proof-shell-retract-files-regexp."
        ;;  str below)
        ;; FIXME: should adjust proof-nesting-depth here.
        ((or (eq (span-property span 'type) 'comment)
+	    (eq (span-property span 'type) 'proverproc)
 	    (eq (span-property span 'type) 'proof); da: needed?
             (proof-string-match isar-undo-skip-regexp str)
             (proof-string-match isar-undo-ignore-regexp str)))
diff --git a/lego/lego.el b/lego/lego.el
index 00a32319..d5b882b9 100644
--- a/lego/lego.el
+++ b/lego/lego.el
@@ -208,6 +208,8 @@ Given is the first SPAN which needs to be undone."
        
        ((eq (span-property span 'type) 'comment))
 
+       ((eq (span-property span 'type) 'proverproc))
+
        ((eq (span-property span 'type) 'goalsave)
 	(unless (eq (span-property span 'name) proof-unnamed-theorem-name)
 	  (setq ans (format lego-forget-id-command (span-property span 'name)))))
diff --git a/phox/phox-fun.el b/phox/phox-fun.el
index d556a3c8..12dddf42 100644
--- a/phox/phox-fun.el
+++ b/phox/phox-fun.el
@@ -177,6 +177,8 @@ or for optional argument TABLE."
 
        ((eq (span-property span 'type) 'comment))       
 
+       ((eq (span-property span 'type) 'proverproc))
+
        ((eq (span-property span 'type) 'goalsave)
 	(if (proof-string-match phox-prove-claim-regexp str)
 	    (setq ans (concat (format phox-forget-proof-command 
@@ -433,4 +435,4 @@ send a delete command to PhoX for the symbol whose name is under the cursor."
 (provide 'phox-fun)
 
 
-    
\ No newline at end of file
+    
diff --git a/plastic/plastic.el b/plastic/plastic.el
index 463ab4ec..c334cf53 100644
--- a/plastic/plastic.el
+++ b/plastic/plastic.el
@@ -244,6 +244,7 @@ Given is the first SPAN which needs to be undone."
     ;;  so that Undo can be implemented via the tmp_cmd route.)
   (let (string (spans 0))
     (while span
+      ;; FIXME da: should probably ignore comments/proverproc here?
       (setq string (span-property span 'cmd))
       (plastic-preprocessing)		;; dynamic scope, on string
 
-- 
cgit v1.2.3