src/Pure/Thy/thy_header.scala

--- a/src/Pure/Thy/thy_header.scala	Sat Jul 09 21:53:27 2011 +0200
+++ b/src/Pure/Thy/thy_header.scala	Sun Jul 10 00:21:19 2011 +0200
@@ -31,6 +31,11 @@
       Header(f(name), imports.map(f), uses.map(f))
   }
 
+  def make_xml_data(header: Header): XML.Body =
+    XML_Data.make_triple(XML_Data.make_string)(
+      XML_Data.make_list(XML_Data.make_string))(
+        XML_Data.make_list(XML_Data.make_string))(header.name, header.imports, header.uses)
+
 
   /* file name */