diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2000-11-24 13:28:13 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2000-11-24 13:28:13 +0000 |
| commit | 22b791f0c77d8063153939cd02295c01b2d20cc4 (patch) | |
| tree | e1876fb657c1424a97a5e7ccdd123fab9a3d18fe | |
| parent | 8121c7a81d656b930443d752ea6e973af7352f7e (diff) | |
Added proof-shell-match-pgip-cmd
| -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)) |