Change PGIP attribute name class->messageclass to avoid Java keyword clash.
--- a/src/Pure/proof_general.ML Thu Sep 15 10:00:01 2005 +0200
+++ b/src/Pure/proof_general.ML Thu Sep 15 10:33:35 2005 +0200
@@ -180,7 +180,7 @@
XML.element
"pgip"
([("tag", pgip_tag),
- ("class", pgip_class),
+ ("messageclass", pgip_class),
("seq", string_of_int (pgip_serial())),
("id", !pgip_id)] @
if_none (Option.map (single o (pair "destid")) (! pgip_refid)) [] @
@@ -1298,7 +1298,7 @@
(case xml of
XML.Elem ("pgip", attrs, pgips) =>
(let
- val class = xmlattr "class" attrs
+ val class = xmlattr "messageclass" attrs
val dest = xmlattro "destid" attrs
val _ = (pgip_refid := xmlattro "id" attrs;
pgip_refseq := xmlattro "seq" attrs)