From ae4ac0d6820e03d5cad6ff11601089fb2880e01b Mon Sep 17 00:00:00 2001
From: Dilip Sequiera
Date: Thu, 21 Nov 1996 15:55:28 +0000
Subject: Synchro bug fixed.

---
 ext.el | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'ext.el')

diff --git a/ext.el b/ext.el
index 023fc13d..b52d8971 100644
--- a/ext.el
+++ b/ext.el
@@ -114,7 +114,6 @@
   (insert-buffer-substring (proof-shell-buffer) start end))
 
 (defun lego-pbp-process-region (pbp-start pbp-end)
-  (message "process")
   (let (start end)
    (save-excursion 
     (goto-char pbp-start)
@@ -132,7 +131,9 @@
       (lego-pbp-sanitise-region pbp-start pbp-end)
       (lego-pbp-display-error start pbp-end))
 
-     ((setq start (search-forward "-- Start of Goals --" pbp-end t))
+     ((search-forward "-- Start of Goals --" pbp-end t)
+      (goto-char pbp-end)
+      (setq start (+ 20 (search-backward "-- Start of Goals --" pbp-start t)))
       (setq end (- (search-forward "-- End of Goals --" pbp-end t) 18))
       (set-buffer lego-goals-buffer)
       (erase-buffer)
@@ -140,7 +141,6 @@
       (lego-pbp-analyse-structure))
 
      ((search-forward "-- Pbp result --" () t)
-      (message "pbp")
       (end-of-line)
       (setq start (point))
       (search-forward "-- End Pbp result --" () t)
@@ -157,7 +157,6 @@
 ;; NEED TO SET LAST_MARK ***BEFORE*** calling process-region 
 
 (defun lego-pbp-filter (string)
-  (message "filter")
   (save-excursion
     (set-buffer (proof-shell-buffer))
 
-- 
cgit v1.2.3