equal
deleted
inserted
replaced
30 def map(f: String => String): Header = |
30 def map(f: String => String): Header = |
31 Header(f(name), imports.map(f), uses.map(f)) |
31 Header(f(name), imports.map(f), uses.map(f)) |
32 } |
32 } |
33 |
33 |
34 def make_xml_data(header: Header): XML.Body = |
34 def make_xml_data(header: Header): XML.Body = |
35 XML_Data.make_triple(XML_Data.make_string)( |
35 XML_Data.make_triple(XML_Data.make_string, |
36 XML_Data.make_list(XML_Data.make_string))( |
36 XML_Data.make_list(XML_Data.make_string), |
37 XML_Data.make_list(XML_Data.make_string))(header.name, header.imports, header.uses) |
37 XML_Data.make_list(XML_Data.make_string))(header.name, header.imports, header.uses) |
38 |
38 |
39 |
39 |
40 /* file name */ |
40 /* file name */ |
41 |
41 |