diff options
| -rw-r--r-- | generic/proof-config.el | 7 | ||||
| -rw-r--r-- | generic/proof-shell.el | 9 |
2 files changed, 16 insertions, 0 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index 176cb84e..8fac7b22 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -1838,6 +1838,13 @@ settings." :type '(choice nil regexp) :group 'proof-shell) +(defcustom proof-shell-match-pgip-cmd nil + "Regexp used to match PGIP command from proof assistant. +The matching string will be parsed as XML and then processed by +`pg-pgip-process-cmd'." + :type '(choice nil regexp) + :group 'proof-shell) + (defcustom proof-shell-theorem-dependency-list-regexp nil "Regexp matching output telling Proof General what the dependencies are. This is so that the dependent theorems can be highlighted somehow. 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)) |