1.1 --- a/src/Pure/ProofGeneral/pgip_output.ML	Tue Dec 05 13:57:24 2006 +0100
     1.2 +++ b/src/Pure/ProofGeneral/pgip_output.ML	Tue Dec 05 14:05:23 2006 +0100
     1.3 @@ -118,7 +118,7 @@
     1.4      in
     1.5          XML.Elem ("normalresponse", 
     1.6                   (attrs_of_displayarea area) @
     1.7 -                 (if urgent then [("urgent", "true")] else []) @
     1.8 +                 (if urgent then attr "urgent" "true" else []) @
     1.9                   (attrs_of_messagecategory messagecategory),
    1.10                   content)
    1.11      end
    1.12 @@ -192,7 +192,7 @@
    1.13  fun idtable vs = 
    1.14      let 
    1.15          val objtype = #objtype vs
    1.16 -        val objtype_attrs = attr [("objtype", objtype)]
    1.17 +        val objtype_attrs = attr "objtype" objtype
    1.18          val context = #context vs
    1.19          val context_attrs = opt_attr "context" context
    1.20          val ids = #ids vs
    1.21 @@ -228,8 +228,8 @@
    1.22  fun acceptedpgipelems vs = 
    1.23      let
    1.24          val pgipelems = #pgipelems vs
    1.25 -        fun async_attrs b = if b then [("async","true")] else []
    1.26 -        fun attrs_attrs attrs = if attrs=[] then [] else [("attributes",space_implode "," attrs)]
    1.27 +        fun async_attrs b = if b then attr "async" "true" else []
    1.28 +        fun attrs_attrs attrs = if attrs=[] then [] else attr "attributes" (space_implode "," attrs)
    1.29          fun singlepgipelem (e,async,attrs) = 
    1.30              XML.Elem("pgipelem", ((async_attrs async) @ (attrs_attrs attrs)),[])
    1.31                                                        
    1.32 @@ -252,7 +252,7 @@
    1.33          val name = #name vs
    1.34          val value = #value vs
    1.35      in
    1.36 -        XML.Elem("prefval", [("name",name)], [XML.Text value])
    1.37 +        XML.Elem("prefval", attr "name" name, [XML.Text value])
    1.38      end 
    1.39  
    1.40  fun idvalue vs =
    1.41 @@ -277,7 +277,7 @@
    1.42        val guisefile = elto "guisefile" attrs_of_pgipurl file
    1.43        val guisetheory = elto "guisetheory" (single o (pair "thyname")) theory
    1.44        val guiseproof = elto "guiseproof" 
    1.45 -                            (fn thm=>[("thmname",thm)]@
    1.46 +                            (fn thm=>(attr "thmname" thm) @
    1.47                                       (opt_attr "proofpos" (Option.map Int.toString proofpos))) theorem
    1.48    in 
    1.49        XML.Elem("informguise", [], guisefile @ guisetheory @ guiseproof)
    1.50 @@ -296,14 +296,14 @@
    1.51          val version = #version vs
    1.52          val acceptedelems = acceptedpgipelems vs
    1.53      in 
    1.54 -        XML.Elem("usespgip", [("version", version)], [acceptedelems])
    1.55 +        XML.Elem("usespgip", attr "version" version, [acceptedelems])
    1.56      end
    1.57  
    1.58  fun usespgml vs =
    1.59      let
    1.60          val version = #version vs
    1.61      in 
    1.62 -        XML.Elem("usespgml", [("version", version)], [])
    1.63 +        XML.Elem("usespgml", attr "version" version, [])
    1.64      end
    1.65  
    1.66  fun pgip vs =
    1.67 @@ -319,12 +319,12 @@
    1.68      in
    1.69          XML.Elem("pgip",
    1.70                   opt_attr "tag" tag @
    1.71 -                 [("id", id)] @
    1.72 +                 attr "id" id @
    1.73                   opt_attr "destid" destid @
    1.74 -                 [("class", class)] @
    1.75 +                 attr "class" class @
    1.76                   opt_attr "refid" refid @
    1.77                   opt_attr_map string_of_int "refseq" refseq @
    1.78 -                 [("seq", string_of_int seq)],
    1.79 +                 attr "seq" (string_of_int seq),
    1.80                   content)
    1.81      end
    1.82