Added proof-shell-match-pgip-cmd

1 files changed, 9 insertions, 0 deletions

diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 9c078c78..73a53f6e 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1415,6 +1415,15 @@ proof-shell-eager-annotation-start, proof-shell-eager-annotation-end."
 	     "setting `" variable "'\n to: \n"
 	     expr "\n"))))))
 
+   ;; CASE PGIP message from proof assistant.
+   ((and proof-shell-match-pgip-cmd
+	 (string-match proof-shell-match-pgip-cmd message))
+    (require 'pg-xml)
+    (require 'pg-pgip)
+    (let
+	((parsed-pgip  (pg-xml-parse-string message)))
+     (pg-pgip-process-cmd parsed-pgip)))
+
    ;; CASE theorem dependency: prover lists thms used in last proof
    ((and proof-shell-theorem-dependency-list-regexp 
 	 (string-match proof-shell-theorem-dependency-list-regexp message))