From b281a871556de5b237ce70290277e8f29017dbb3 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 14 Nov 2002 00:40:52 +0000
Subject: Tweak calling of pg-pgip processing commands.

---
 generic/proof-shell.el | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

(limited to 'generic')

diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index fdf9259c..a6b33f6c 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1260,9 +1260,21 @@ MESSAGE should be a string annotated with
 	   (string-match proof-shell-match-pgip-cmd message))
       (require 'pg-xml)
       (require 'pg-pgip)
+      (unless (string-match (match-string 0)
+			    proof-shell-eager-annotation-start)
+	;; Assume that eager annotation regexps are _not_ part of PGIP
+	;; message, and strip them.  This allows hybrid PGIP/non PGIP
+	;; communication, with PGIP embedded in urgent messages.
+	(setq message
+	      (substring 
+	       message
+	       (progn
+		 (string-match proof-shell-eager-annotation-start message)
+		 (match-end 0))
+	       (string-match proof-shell-eager-annotation-end message))))
       (let
 	  ((parsed-pgip  (pg-xml-parse-string message)))
-	(pg-pgip-process-cmd parsed-pgip)))
+	(pg-pgip-process-packet parsed-pgip)))
      
      ;; CASE theorem dependency: prover lists thms used in last proof
      ((and proof-shell-theorem-dependency-list-regexp 
-- 
cgit v1.2.3