# HG changeset patch
# User aspinall
# Date 1126773215 -7200
# Node ID de60322ff13a4c8cd06ec60ede0b820cf057d11c
# Parent  41f1249bce372230ee58fa9eedefc9b3b9466f79
Change PGIP attribute name class->messageclass to avoid Java keyword clash.

diff -r 41f1249bce37 -r de60322ff13a 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)