src/Pure/Thy/thy_header.scala
changeset 43722 9b5dadb0c28d
parent 43699 fb3d99df4b1e
child 43723 8a63c95b1d5b
     1.1 --- a/src/Pure/Thy/thy_header.scala	Sat Jul 09 21:53:27 2011 +0200
     1.2 +++ b/src/Pure/Thy/thy_header.scala	Sun Jul 10 00:21:19 2011 +0200
     1.3 @@ -31,6 +31,11 @@
     1.4        Header(f(name), imports.map(f), uses.map(f))
     1.5    }
     1.6  
     1.7 +  def make_xml_data(header: Header): XML.Body =
     1.8 +    XML_Data.make_triple(XML_Data.make_string)(
     1.9 +      XML_Data.make_list(XML_Data.make_string))(
    1.10 +        XML_Data.make_list(XML_Data.make_string))(header.name, header.imports, header.uses)
    1.11 +
    1.12  
    1.13    /* file name */
    1.14