src/Pure/Tools/xml_syntax.ML
changeset 21645 4af699cdfe47
parent 20658 2586df9fb95a
child 23831 64e6e5c738a1
equal deleted inserted replaced
21644:5154a7213d3c 21645:4af699cdfe47
     9 signature XML_SYNTAX =
     9 signature XML_SYNTAX =
    10 sig
    10 sig
    11   val xml_of_type: typ -> XML.tree
    11   val xml_of_type: typ -> XML.tree
    12   val xml_of_term: term -> XML.tree
    12   val xml_of_term: term -> XML.tree
    13   val xml_of_proof: Proofterm.proof -> XML.tree
    13   val xml_of_proof: Proofterm.proof -> XML.tree
    14   val write_to_file: string -> string -> XML.tree -> unit
    14   val write_to_file: Path.T -> string -> XML.tree -> unit
    15   exception XML of string * XML.tree
    15   exception XML of string * XML.tree
    16   val type_of_xml: XML.tree -> typ
    16   val type_of_xml: XML.tree -> typ
    17   val term_of_xml: XML.tree -> term
    17   val term_of_xml: XML.tree -> term
    18   val proof_of_xml: XML.tree -> Proofterm.proof
    18   val proof_of_xml: XML.tree -> Proofterm.proof
    19 end;
    19 end;
    69         xml_of_proof prf ::
    69         xml_of_proof prf ::
    70         (case optt of NONE => [] | SOME t => [xml_of_term t]))
    70         (case optt of NONE => [] | SOME t => [xml_of_term t]))
    71   | xml_of_proof (prf %% prf') =
    71   | xml_of_proof (prf %% prf') =
    72       XML.Elem ("AppP", [], [xml_of_proof prf, xml_of_proof prf'])
    72       XML.Elem ("AppP", [], [xml_of_proof prf, xml_of_proof prf'])
    73   | xml_of_proof (Hyp t) = XML.Elem ("Hyp", [], [xml_of_term t])
    73   | xml_of_proof (Hyp t) = XML.Elem ("Hyp", [], [xml_of_term t])
    74   | xml_of_proof (PThm ((s, _), _, t, optTs)) =
    74   | xml_of_proof (PThm (s, _, t, optTs)) =
    75       XML.Elem ("PThm", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
    75       XML.Elem ("PThm", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
    76   | xml_of_proof (PAxm (s, t, optTs)) =
    76   | xml_of_proof (PAxm (s, t, optTs)) =
    77       XML.Elem ("PAxm", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
    77       XML.Elem ("PAxm", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
    78   | xml_of_proof (Oracle (s, t, optTs)) =
    78   | xml_of_proof (Oracle (s, t, optTs)) =
    79       XML.Elem ("Oracle", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
    79       XML.Elem ("Oracle", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
    80   | xml_of_proof (MinProof prfs) =
    80   | xml_of_proof (MinProof prfs) =
    81       XML.Elem ("MinProof", [], []);
    81       XML.Elem ("MinProof", [], []);
    82 
    82 
    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 fname elname x =
    85 fun write_to_file path elname x =
    86   File.write (Path.unpack fname)
    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_tree (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])));
   153   | proof_of_xml (XML.Elem ("Appt", [], [proof, term])) =
   153   | proof_of_xml (XML.Elem ("Appt", [], [proof, term])) =
   154       proof_of_xml proof % SOME (term_of_xml term)
   154       proof_of_xml proof % SOME (term_of_xml term)
   155   | proof_of_xml (XML.Elem ("AppP", [], [proof, proof'])) =
   155   | proof_of_xml (XML.Elem ("AppP", [], [proof, proof'])) =
   156       proof_of_xml proof %% proof_of_xml proof'
   156       proof_of_xml proof %% proof_of_xml proof'
   157   | proof_of_xml (XML.Elem ("PThm", [("name", s)], term :: opttypes)) =
   157   | proof_of_xml (XML.Elem ("PThm", [("name", s)], term :: opttypes)) =
   158       PThm ((s, []), MinProof ([], [], []),  (* FIXME? *)
   158       PThm (s, MinProof ([], [], []),  (* FIXME? *)
   159         term_of_xml term, opttypes_of_xml opttypes)
   159         term_of_xml term, opttypes_of_xml opttypes)
   160   | proof_of_xml (XML.Elem ("PAxm", [("name", s)], term :: opttypes)) =
   160   | proof_of_xml (XML.Elem ("PAxm", [("name", s)], term :: opttypes)) =
   161       PAxm (s, term_of_xml term, opttypes_of_xml opttypes)
   161       PAxm (s, term_of_xml term, opttypes_of_xml opttypes)
   162   | proof_of_xml (XML.Elem ("Oracle", [("name", s)], term :: opttypes)) =
   162   | proof_of_xml (XML.Elem ("Oracle", [("name", s)], term :: opttypes)) =
   163       Oracle (s, term_of_xml term, opttypes_of_xml opttypes)
   163       Oracle (s, term_of_xml term, opttypes_of_xml opttypes)