equal
deleted
inserted
replaced
83 (* useful for checking the output against a schema file *) |
83 (* useful for checking the output against a schema file *) |
84 |
84 |
85 fun write_to_file path elname x = |
85 fun write_to_file path elname x = |
86 File.write path |
86 File.write path |
87 ("<?xml version=\"1.0\" encoding=\"UTF-8\"?>\n" ^ |
87 ("<?xml version=\"1.0\" encoding=\"UTF-8\"?>\n" ^ |
88 XML.string_of_tree (XML.Elem (elname, |
88 XML.string_of (XML.Elem (elname, |
89 [("xmlns:xsi", "http://www.w3.org/2001/XMLSchema-instance"), |
89 [("xmlns:xsi", "http://www.w3.org/2001/XMLSchema-instance"), |
90 ("xsi:noNamespaceSchemaLocation", "isabelle.xsd")], |
90 ("xsi:noNamespaceSchemaLocation", "isabelle.xsd")], |
91 [x]))); |
91 [x]))); |
92 |
92 |
93 |
93 |