diff options
| -rw-r--r-- | generic/pg-pgip.el | 9 | ||||
| -rw-r--r-- | generic/pg-xml.el | 3 |
2 files changed, 7 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' - - diff --git a/generic/pg-xml.el b/generic/pg-xml.el index 31ba1515..a305df0f 100644 --- a/generic/pg-xml.el +++ b/generic/pg-xml.el @@ -8,6 +8,8 @@ ;; ;; XML functions for Proof General ;; +;; STATUS: Experimental, not in use. +;; ;; Proof General Kit uses PGIP, an XML-message protocol ;; for interactive proof. The simple functions here allow ;; parsing and writing of XML documents. Little attempt @@ -165,6 +167,7 @@ is (message "Parsing %s...done" (buffer-name buffer))) (caar xmlparse)))) +;;;###autoload (defun pg-xml-parse-string (arg) "Parse string in ARG, same as pg-xml-parse-buffer." (let |