src/Pure/Tools/xml_syntax.ML
changeset 26544 af4c77a21c06
parent 23831 64e6e5c738a1
child 28017 4919bd124a58
equal deleted inserted replaced
26543:cd01c8eb314a 26544:af4c77a21c06
    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