diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2004-08-31 08:05:17 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2004-08-31 08:05:17 +0000 |
commit | 3de6ef498153712d66f48b25b82e251d33869e5f (patch) | |
tree | 08422594150df3a7d0038c43e1e378cad06ad1eb /generic/pg-pgip.el | |
parent | 803614383b7247bd7dd7739cc24749de245ae7c9 (diff) |
Fix backward compatibility with Isabelle 2004.
Diffstat (limited to 'generic/pg-pgip.el')
-rw-r--r-- | generic/pg-pgip.el | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/generic/pg-pgip.el b/generic/pg-pgip.el index e46b4c33..b44bf7e1 100644 --- a/generic/pg-pgip.el +++ b/generic/pg-pgip.el @@ -39,13 +39,16 @@ The list PGIPS may contain one or more PGIP packets, whose contents are processe (defun pg-pgip-process-pgip (pgip) "Process the commands in the PGIP XML-node PGIP." + ;; FIXME: appearances of 'notreallyoptional below should be removed, + ;; but they are needed for compatibility with Isabelle 2004 whose + ;; PGIP messages are incomplete. (let* ((name (xml-node-name pgip)) (origin (pg-xml-get-attr 'origin pgip 'optional)) (id (pg-xml-get-attr 'id pgip 'optional)) - (class (pg-xml-get-attr 'class pgip)) + (class (pg-xml-get-attr 'class pgip 'notreallyoptional)) (refseq (pg-xml-get-attr 'refseq pgip 'optional)) (refid (pg-xml-get-attr 'refid pgip 'optional)) - (seq (pg-xml-get-attr 'seq pgip))) + (seq (pg-xml-get-attr 'seq pgip 'notreallyoptional))) (setq pg-pgip-last-seen-id id) (setq pg-pgip-last-seen-seq seq) (if (eq name 'pgip) @@ -60,7 +63,8 @@ Return a symbol representing the PGIP command processed, or nil." (fname (intern (concat "pg-pgip-process-" (symbol-name name))))) (if (fboundp fname) (progn - (pg-pgip-debug "Processing PGIP message seq %s, type %s" (pg-xml-get-attr 'seq pgip) name) + (pg-pgip-debug "Processing PGIP message seq %s, type %s" + (pg-xml-get-attr 'seq pgip 'notreallyoptional) name) (funcall fname pgipmsg) name) (pg-internal-warning "!!! unrecognized/unimplemented PGIP message element `%s'" name) @@ -68,6 +72,7 @@ Return a symbol representing the PGIP command processed, or nil." (defvar pg-pgip-post-process-functions '((hasprefs . proof-assistant-menu-update) + (oldhaspref . proof-assistant-menu-update) ;; FIXME: for Isabelle2004 backward compat (menuadd . proof-assistant-menu-update) (menudel . proof-assistant-menu-update) (idtable . pg-pgip-update-idtables) ;; TODO: not yet implemented |