Change PGIP attribute name class->messageclass to avoid Java keyword clash.
authoraspinall
Thu, 15 Sep 2005 10:33:35 +0200
changeset 17403 de60322ff13a
parent 17402 41f1249bce37
child 17404 d16c3a62c396
Change PGIP attribute name class->messageclass to avoid Java keyword clash.
src/Pure/proof_general.ML
--- 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)