--- a/src/Pure/ROOT Mon Nov 26 16:22:29 2012 +0100
+++ b/src/Pure/ROOT Mon Nov 26 16:28:22 2012 +0100
@@ -200,7 +200,7 @@
"Thy/thy_output.ML"
"Thy/thy_syntax.ML"
"Tools/named_thms.ML"
- "Tools/xml_syntax.ML"
+ "Tools/legacy_xml_syntax.ML"
"assumption.ML"
"axclass.ML"
"config.ML"
--- a/src/Pure/ROOT.ML Mon Nov 26 16:22:29 2012 +0100
+++ b/src/Pure/ROOT.ML Mon Nov 26 16:28:22 2012 +0100
@@ -283,7 +283,7 @@
use "Tools/named_thms.ML";
-use "Tools/xml_syntax.ML";
+use "Tools/legacy_xml_syntax.ML";
(* configuration for Proof General *)
--- a/src/Pure/Tools/find_theorems.ML Mon Nov 26 16:22:29 2012 +0100
+++ b/src/Pure/Tools/find_theorems.ML Mon Nov 26 16:28:22 2012 +0100
@@ -116,17 +116,17 @@
| xml_of_criterion Elim = XML.Elem (("Elim", []) , [])
| xml_of_criterion Dest = XML.Elem (("Dest", []) , [])
| xml_of_criterion Solves = XML.Elem (("Solves", []) , [])
- | xml_of_criterion (Simp pat) = XML.Elem (("Simp", []) , [XML_Syntax.xml_of_term pat])
- | xml_of_criterion (Pattern pat) = XML.Elem (("Pattern", []) , [XML_Syntax.xml_of_term pat]);
+ | xml_of_criterion (Simp pat) = XML.Elem (("Simp", []), [Legacy_XML_Syntax.xml_of_term pat])
+ | xml_of_criterion (Pattern pat) = XML.Elem (("Pattern", []), [Legacy_XML_Syntax.xml_of_term pat]);
fun criterion_of_xml (XML.Elem (("Name", [("val", name)]), [])) = Name name
| criterion_of_xml (XML.Elem (("Intro", []) , [])) = Intro
| criterion_of_xml (XML.Elem (("Elim", []) , [])) = Elim
| criterion_of_xml (XML.Elem (("Dest", []) , [])) = Dest
| criterion_of_xml (XML.Elem (("Solves", []) , [])) = Solves
- | criterion_of_xml (XML.Elem (("Simp", []) , [tree])) = Simp (XML_Syntax.term_of_xml tree)
- | criterion_of_xml (XML.Elem (("Pattern", []) , [tree])) = Pattern (XML_Syntax.term_of_xml tree)
- | criterion_of_xml tree = raise XML_Syntax.XML ("criterion_of_xml: bad tree", tree);
+ | criterion_of_xml (XML.Elem (("Simp", []), [tree])) = Simp (Legacy_XML_Syntax.term_of_xml tree)
+ | criterion_of_xml (XML.Elem (("Pattern", []), [tree])) = Pattern (Legacy_XML_Syntax.term_of_xml tree)
+ | criterion_of_xml tree = raise Legacy_XML_Syntax.XML ("criterion_of_xml: bad tree", tree);
fun xml_of_query {goal = NONE, limit, rem_dups, criteria} =
let
@@ -149,7 +149,7 @@
in
{goal = NONE, limit = limit, rem_dups = rem_dups, criteria = criteria}
end
- | query_of_xml tree = raise XML_Syntax.XML ("query_of_xml: bad tree", tree);
+ | query_of_xml tree = raise Legacy_XML_Syntax.XML ("query_of_xml: bad tree", tree);
@@ -167,7 +167,7 @@
fun xml_of_theorem (Internal _) = raise Fail "xml_of_theorem: Internal"
| xml_of_theorem (External (fact_ref, prop)) =
- XML.Elem (fact_ref_markup fact_ref ("External", []), [XML_Syntax.xml_of_term prop]);
+ XML.Elem (fact_ref_markup fact_ref ("External", []), [Legacy_XML_Syntax.xml_of_term prop]);
fun theorem_of_xml (XML.Elem (("External", properties), [tree])) =
let
@@ -177,9 +177,9 @@
Option.map (single o Facts.Single o Markup.parse_int)
(Properties.get properties "index");
in
- External (Facts.Named ((name, pos), intvs_opt), XML_Syntax.term_of_xml tree)
+ External (Facts.Named ((name, pos), intvs_opt), Legacy_XML_Syntax.term_of_xml tree)
end
- | theorem_of_xml tree = raise XML_Syntax.XML ("theorem_of_xml: bad tree", tree);
+ | theorem_of_xml tree = raise Legacy_XML_Syntax.XML ("theorem_of_xml: bad tree", tree);
fun xml_of_result (opt_found, theorems) =
let
@@ -192,7 +192,7 @@
fun result_of_xml (XML.Elem (("Result", properties), body)) =
(Properties.get properties "found" |> Option.map Markup.parse_int,
XML.Decode.list (theorem_of_xml o the_single) body)
- | result_of_xml tree = raise XML_Syntax.XML ("result_of_xml: bad tree", tree);
+ | result_of_xml tree = raise Legacy_XML_Syntax.XML ("result_of_xml: bad tree", tree);
fun prop_of (Internal (_, thm)) = Thm.full_prop_of thm
| prop_of (External (_, prop)) = prop;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/legacy_xml_syntax.ML Mon Nov 26 16:28:22 2012 +0100
@@ -0,0 +1,173 @@
+(* Title: Pure/Tools/legacy_xml_syntax.ML
+ Author: Stefan Berghofer, TU Muenchen
+
+Input and output of types, terms, and proofs in XML format.
+See isabelle.xsd for a description of the syntax.
+
+Legacy module, see Pure/term_xml.ML etc.
+*)
+
+signature LEGACY_XML_SYNTAX =
+sig
+ val xml_of_type: typ -> XML.tree
+ val xml_of_term: term -> XML.tree
+ val xml_of_proof: Proofterm.proof -> XML.tree
+ val write_to_file: Path.T -> string -> XML.tree -> unit
+ exception XML of string * XML.tree
+ val type_of_xml: XML.tree -> typ
+ val term_of_xml: XML.tree -> term
+ val proof_of_xml: XML.tree -> Proofterm.proof
+end;
+
+structure Legacy_XML_Syntax : LEGACY_XML_SYNTAX =
+struct
+
+(**** XML output ****)
+
+fun xml_of_class name = XML.Elem (("class", [("name", name)]), []);
+
+fun xml_of_type (TVar ((s, i), S)) =
+ XML.Elem (("TVar", ("name", s) :: (if i=0 then [] else [("index", string_of_int i)])),
+ map xml_of_class S)
+ | xml_of_type (TFree (s, S)) =
+ XML.Elem (("TFree", [("name", s)]), map xml_of_class S)
+ | xml_of_type (Type (s, Ts)) =
+ XML.Elem (("Type", [("name", s)]), map xml_of_type Ts);
+
+fun xml_of_term (Bound i) =
+ XML.Elem (("Bound", [("index", string_of_int i)]), [])
+ | xml_of_term (Free (s, T)) =
+ XML.Elem (("Free", [("name", s)]), [xml_of_type T])
+ | xml_of_term (Var ((s, i), T)) =
+ XML.Elem (("Var", ("name", s) :: (if i=0 then [] else [("index", string_of_int i)])),
+ [xml_of_type T])
+ | xml_of_term (Const (s, T)) =
+ XML.Elem (("Const", [("name", s)]), [xml_of_type T])
+ | xml_of_term (t $ u) =
+ XML.Elem (("App", []), [xml_of_term t, xml_of_term u])
+ | xml_of_term (Abs (s, T, t)) =
+ XML.Elem (("Abs", [("vname", s)]), [xml_of_type T, xml_of_term t]);
+
+fun xml_of_opttypes NONE = []
+ | xml_of_opttypes (SOME Ts) = [XML.Elem (("types", []), map xml_of_type Ts)];
+
+(* FIXME: the t argument of PThm and PAxm is actually redundant, since *)
+(* it can be looked up in the theorem database. Thus, it could be *)
+(* omitted from the xml representation. *)
+
+(* FIXME not exhaustive *)
+fun xml_of_proof (PBound i) =
+ XML.Elem (("PBound", [("index", string_of_int i)]), [])
+ | xml_of_proof (Abst (s, optT, prf)) =
+ XML.Elem (("Abst", [("vname", s)]),
+ (case optT of NONE => [] | SOME T => [xml_of_type T]) @ [xml_of_proof prf])
+ | xml_of_proof (AbsP (s, optt, prf)) =
+ XML.Elem (("AbsP", [("vname", s)]),
+ (case optt of NONE => [] | SOME t => [xml_of_term t]) @ [xml_of_proof prf])
+ | xml_of_proof (prf % optt) =
+ XML.Elem (("Appt", []),
+ xml_of_proof prf :: (case optt of NONE => [] | SOME t => [xml_of_term t]))
+ | xml_of_proof (prf %% prf') =
+ XML.Elem (("AppP", []), [xml_of_proof prf, xml_of_proof prf'])
+ | xml_of_proof (Hyp t) = XML.Elem (("Hyp", []), [xml_of_term t])
+ | xml_of_proof (PThm (_, ((s, t, optTs), _))) =
+ XML.Elem (("PThm", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
+ | xml_of_proof (PAxm (s, t, optTs)) =
+ XML.Elem (("PAxm", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
+ | xml_of_proof (Oracle (s, t, optTs)) =
+ XML.Elem (("Oracle", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
+ | xml_of_proof MinProof =
+ XML.Elem (("MinProof", []), []);
+
+
+(* useful for checking the output against a schema file *)
+
+fun write_to_file path elname x =
+ File.write path
+ ("<?xml version=\"1.0\" encoding=\"UTF-8\"?>\n" ^
+ XML.string_of (XML.Elem ((elname,
+ [("xmlns:xsi", "http://www.w3.org/2001/XMLSchema-instance"),
+ ("xsi:noNamespaceSchemaLocation", "isabelle.xsd")]),
+ [x])));
+
+
+
+(**** XML input ****)
+
+exception XML of string * XML.tree;
+
+fun class_of_xml (XML.Elem (("class", [("name", name)]), [])) = name
+ | class_of_xml tree = raise XML ("class_of_xml: bad tree", tree);
+
+fun index_of_string s tree idx =
+ (case Int.fromString idx of
+ NONE => raise XML (s ^ ": bad index", tree)
+ | SOME i => i);
+
+fun type_of_xml (tree as XML.Elem (("TVar", atts), classes)) = TVar
+ ((case Properties.get atts "name" of
+ NONE => raise XML ("type_of_xml: name of TVar missing", tree)
+ | SOME name => name,
+ the_default 0 (Option.map (index_of_string "type_of_xml" tree)
+ (Properties.get atts "index"))),
+ map class_of_xml classes)
+ | type_of_xml (XML.Elem (("TFree", [("name", s)]), classes)) =
+ TFree (s, map class_of_xml classes)
+ | type_of_xml (XML.Elem (("Type", [("name", s)]), types)) =
+ Type (s, map type_of_xml types)
+ | type_of_xml tree = raise XML ("type_of_xml: bad tree", tree);
+
+fun term_of_xml (tree as XML.Elem (("Bound", [("index", idx)]), [])) =
+ Bound (index_of_string "bad variable index" tree idx)
+ | term_of_xml (XML.Elem (("Free", [("name", s)]), [typ])) =
+ Free (s, type_of_xml typ)
+ | term_of_xml (tree as XML.Elem (("Var", atts), [typ])) = Var
+ ((case Properties.get atts "name" of
+ NONE => raise XML ("type_of_xml: name of Var missing", tree)
+ | SOME name => name,
+ the_default 0 (Option.map (index_of_string "term_of_xml" tree)
+ (Properties.get atts "index"))),
+ type_of_xml typ)
+ | term_of_xml (XML.Elem (("Const", [("name", s)]), [typ])) =
+ Const (s, type_of_xml typ)
+ | term_of_xml (XML.Elem (("App", []), [term, term'])) =
+ term_of_xml term $ term_of_xml term'
+ | term_of_xml (XML.Elem (("Abs", [("vname", s)]), [typ, term])) =
+ Abs (s, type_of_xml typ, term_of_xml term)
+ | term_of_xml tree = raise XML ("term_of_xml: bad tree", tree);
+
+fun opttypes_of_xml [] = NONE
+ | opttypes_of_xml [XML.Elem (("types", []), types)] =
+ SOME (map type_of_xml types)
+ | opttypes_of_xml (tree :: _) = raise XML ("opttypes_of_xml: bad tree", tree);
+
+fun proof_of_xml (tree as XML.Elem (("PBound", [("index", idx)]), [])) =
+ PBound (index_of_string "proof_of_xml" tree idx)
+ | proof_of_xml (XML.Elem (("Abst", [("vname", s)]), [proof])) =
+ Abst (s, NONE, proof_of_xml proof)
+ | proof_of_xml (XML.Elem (("Abst", [("vname", s)]), [typ, proof])) =
+ Abst (s, SOME (type_of_xml typ), proof_of_xml proof)
+ | proof_of_xml (XML.Elem (("AbsP", [("vname", s)]), [proof])) =
+ AbsP (s, NONE, proof_of_xml proof)
+ | proof_of_xml (XML.Elem (("AbsP", [("vname", s)]), [term, proof])) =
+ AbsP (s, SOME (term_of_xml term), proof_of_xml proof)
+ | proof_of_xml (XML.Elem (("Appt", []), [proof])) =
+ proof_of_xml proof % NONE
+ | proof_of_xml (XML.Elem (("Appt", []), [proof, term])) =
+ proof_of_xml proof % SOME (term_of_xml term)
+ | proof_of_xml (XML.Elem (("AppP", []), [proof, proof'])) =
+ proof_of_xml proof %% proof_of_xml proof'
+ | proof_of_xml (XML.Elem (("Hyp", []), [term])) =
+ Hyp (term_of_xml term)
+ | proof_of_xml (XML.Elem (("PThm", [("name", s)]), term :: opttypes)) =
+ (* FIXME? *)
+ PThm (serial (), ((s, term_of_xml term, opttypes_of_xml opttypes),
+ Future.value (Proofterm.approximate_proof_body MinProof)))
+ | proof_of_xml (XML.Elem (("PAxm", [("name", s)]), term :: opttypes)) =
+ PAxm (s, term_of_xml term, opttypes_of_xml opttypes)
+ | proof_of_xml (XML.Elem (("Oracle", [("name", s)]), term :: opttypes)) =
+ Oracle (s, term_of_xml term, opttypes_of_xml opttypes)
+ | proof_of_xml (XML.Elem (("MinProof", _), _)) = MinProof
+ | proof_of_xml tree = raise XML ("proof_of_xml: bad tree", tree);
+
+end;
--- a/src/Pure/Tools/xml_syntax.ML Mon Nov 26 16:22:29 2012 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,171 +0,0 @@
-(* Title: Pure/Tools/xml_syntax.ML
- Author: Stefan Berghofer, TU Muenchen
-
-Input and output of types, terms, and proofs in XML format.
-See isabelle.xsd for a description of the syntax.
-*)
-
-signature XML_SYNTAX =
-sig
- val xml_of_type: typ -> XML.tree
- val xml_of_term: term -> XML.tree
- val xml_of_proof: Proofterm.proof -> XML.tree
- val write_to_file: Path.T -> string -> XML.tree -> unit
- exception XML of string * XML.tree
- val type_of_xml: XML.tree -> typ
- val term_of_xml: XML.tree -> term
- val proof_of_xml: XML.tree -> Proofterm.proof
-end;
-
-structure XML_Syntax : XML_SYNTAX =
-struct
-
-(**** XML output ****)
-
-fun xml_of_class name = XML.Elem (("class", [("name", name)]), []);
-
-fun xml_of_type (TVar ((s, i), S)) =
- XML.Elem (("TVar", ("name", s) :: (if i=0 then [] else [("index", string_of_int i)])),
- map xml_of_class S)
- | xml_of_type (TFree (s, S)) =
- XML.Elem (("TFree", [("name", s)]), map xml_of_class S)
- | xml_of_type (Type (s, Ts)) =
- XML.Elem (("Type", [("name", s)]), map xml_of_type Ts);
-
-fun xml_of_term (Bound i) =
- XML.Elem (("Bound", [("index", string_of_int i)]), [])
- | xml_of_term (Free (s, T)) =
- XML.Elem (("Free", [("name", s)]), [xml_of_type T])
- | xml_of_term (Var ((s, i), T)) =
- XML.Elem (("Var", ("name", s) :: (if i=0 then [] else [("index", string_of_int i)])),
- [xml_of_type T])
- | xml_of_term (Const (s, T)) =
- XML.Elem (("Const", [("name", s)]), [xml_of_type T])
- | xml_of_term (t $ u) =
- XML.Elem (("App", []), [xml_of_term t, xml_of_term u])
- | xml_of_term (Abs (s, T, t)) =
- XML.Elem (("Abs", [("vname", s)]), [xml_of_type T, xml_of_term t]);
-
-fun xml_of_opttypes NONE = []
- | xml_of_opttypes (SOME Ts) = [XML.Elem (("types", []), map xml_of_type Ts)];
-
-(* FIXME: the t argument of PThm and PAxm is actually redundant, since *)
-(* it can be looked up in the theorem database. Thus, it could be *)
-(* omitted from the xml representation. *)
-
-(* FIXME not exhaustive *)
-fun xml_of_proof (PBound i) =
- XML.Elem (("PBound", [("index", string_of_int i)]), [])
- | xml_of_proof (Abst (s, optT, prf)) =
- XML.Elem (("Abst", [("vname", s)]),
- (case optT of NONE => [] | SOME T => [xml_of_type T]) @ [xml_of_proof prf])
- | xml_of_proof (AbsP (s, optt, prf)) =
- XML.Elem (("AbsP", [("vname", s)]),
- (case optt of NONE => [] | SOME t => [xml_of_term t]) @ [xml_of_proof prf])
- | xml_of_proof (prf % optt) =
- XML.Elem (("Appt", []),
- xml_of_proof prf :: (case optt of NONE => [] | SOME t => [xml_of_term t]))
- | xml_of_proof (prf %% prf') =
- XML.Elem (("AppP", []), [xml_of_proof prf, xml_of_proof prf'])
- | xml_of_proof (Hyp t) = XML.Elem (("Hyp", []), [xml_of_term t])
- | xml_of_proof (PThm (_, ((s, t, optTs), _))) =
- XML.Elem (("PThm", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
- | xml_of_proof (PAxm (s, t, optTs)) =
- XML.Elem (("PAxm", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
- | xml_of_proof (Oracle (s, t, optTs)) =
- XML.Elem (("Oracle", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
- | xml_of_proof MinProof =
- XML.Elem (("MinProof", []), []);
-
-
-(* useful for checking the output against a schema file *)
-
-fun write_to_file path elname x =
- File.write path
- ("<?xml version=\"1.0\" encoding=\"UTF-8\"?>\n" ^
- XML.string_of (XML.Elem ((elname,
- [("xmlns:xsi", "http://www.w3.org/2001/XMLSchema-instance"),
- ("xsi:noNamespaceSchemaLocation", "isabelle.xsd")]),
- [x])));
-
-
-
-(**** XML input ****)
-
-exception XML of string * XML.tree;
-
-fun class_of_xml (XML.Elem (("class", [("name", name)]), [])) = name
- | class_of_xml tree = raise XML ("class_of_xml: bad tree", tree);
-
-fun index_of_string s tree idx =
- (case Int.fromString idx of
- NONE => raise XML (s ^ ": bad index", tree)
- | SOME i => i);
-
-fun type_of_xml (tree as XML.Elem (("TVar", atts), classes)) = TVar
- ((case Properties.get atts "name" of
- NONE => raise XML ("type_of_xml: name of TVar missing", tree)
- | SOME name => name,
- the_default 0 (Option.map (index_of_string "type_of_xml" tree)
- (Properties.get atts "index"))),
- map class_of_xml classes)
- | type_of_xml (XML.Elem (("TFree", [("name", s)]), classes)) =
- TFree (s, map class_of_xml classes)
- | type_of_xml (XML.Elem (("Type", [("name", s)]), types)) =
- Type (s, map type_of_xml types)
- | type_of_xml tree = raise XML ("type_of_xml: bad tree", tree);
-
-fun term_of_xml (tree as XML.Elem (("Bound", [("index", idx)]), [])) =
- Bound (index_of_string "bad variable index" tree idx)
- | term_of_xml (XML.Elem (("Free", [("name", s)]), [typ])) =
- Free (s, type_of_xml typ)
- | term_of_xml (tree as XML.Elem (("Var", atts), [typ])) = Var
- ((case Properties.get atts "name" of
- NONE => raise XML ("type_of_xml: name of Var missing", tree)
- | SOME name => name,
- the_default 0 (Option.map (index_of_string "term_of_xml" tree)
- (Properties.get atts "index"))),
- type_of_xml typ)
- | term_of_xml (XML.Elem (("Const", [("name", s)]), [typ])) =
- Const (s, type_of_xml typ)
- | term_of_xml (XML.Elem (("App", []), [term, term'])) =
- term_of_xml term $ term_of_xml term'
- | term_of_xml (XML.Elem (("Abs", [("vname", s)]), [typ, term])) =
- Abs (s, type_of_xml typ, term_of_xml term)
- | term_of_xml tree = raise XML ("term_of_xml: bad tree", tree);
-
-fun opttypes_of_xml [] = NONE
- | opttypes_of_xml [XML.Elem (("types", []), types)] =
- SOME (map type_of_xml types)
- | opttypes_of_xml (tree :: _) = raise XML ("opttypes_of_xml: bad tree", tree);
-
-fun proof_of_xml (tree as XML.Elem (("PBound", [("index", idx)]), [])) =
- PBound (index_of_string "proof_of_xml" tree idx)
- | proof_of_xml (XML.Elem (("Abst", [("vname", s)]), [proof])) =
- Abst (s, NONE, proof_of_xml proof)
- | proof_of_xml (XML.Elem (("Abst", [("vname", s)]), [typ, proof])) =
- Abst (s, SOME (type_of_xml typ), proof_of_xml proof)
- | proof_of_xml (XML.Elem (("AbsP", [("vname", s)]), [proof])) =
- AbsP (s, NONE, proof_of_xml proof)
- | proof_of_xml (XML.Elem (("AbsP", [("vname", s)]), [term, proof])) =
- AbsP (s, SOME (term_of_xml term), proof_of_xml proof)
- | proof_of_xml (XML.Elem (("Appt", []), [proof])) =
- proof_of_xml proof % NONE
- | proof_of_xml (XML.Elem (("Appt", []), [proof, term])) =
- proof_of_xml proof % SOME (term_of_xml term)
- | proof_of_xml (XML.Elem (("AppP", []), [proof, proof'])) =
- proof_of_xml proof %% proof_of_xml proof'
- | proof_of_xml (XML.Elem (("Hyp", []), [term])) =
- Hyp (term_of_xml term)
- | proof_of_xml (XML.Elem (("PThm", [("name", s)]), term :: opttypes)) =
- (* FIXME? *)
- PThm (serial (), ((s, term_of_xml term, opttypes_of_xml opttypes),
- Future.value (Proofterm.approximate_proof_body MinProof)))
- | proof_of_xml (XML.Elem (("PAxm", [("name", s)]), term :: opttypes)) =
- PAxm (s, term_of_xml term, opttypes_of_xml opttypes)
- | proof_of_xml (XML.Elem (("Oracle", [("name", s)]), term :: opttypes)) =
- Oracle (s, term_of_xml term, opttypes_of_xml opttypes)
- | proof_of_xml (XML.Elem (("MinProof", _), _)) = MinProof
- | proof_of_xml tree = raise XML ("proof_of_xml: bad tree", tree);
-
-end;