diff options
Diffstat (limited to 'generic/pg-pgip.el')
| -rw-r--r-- | generic/pg-pgip.el | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/generic/pg-pgip.el b/generic/pg-pgip.el index 963c6fd0..b35941c6 100644 --- a/generic/pg-pgip.el +++ b/generic/pg-pgip.el @@ -6,11 +6,14 @@ ;; ;; $Id$ ;; +;; STATUS: Experimental, not in use. +;; ;; Proof General Kit uses PGIP, an XML-message protocol ;; for interactive proof. This file contains functions ;; to process PGIP commands sent from the proof assistant. ;; +;;;###autoload (defun pg-pgip-process-cmd (pgip) "Process the command in PGIP, which should be parsed XML according to pg-xml-parse-*." (while (pgip) @@ -120,11 +123,7 @@ (pg-pgip-get-attr elt "version" attrs optional)) - - - +(provide 'pg-pgip) ;; End of `pg-pgip.el' - - |