# HG changeset patch # User wenzelm # Date 1375998755 -7200 # Node ID 6415d95bf7a29c451b725b6bdb47764124eff741 # Parent 71e938856a03edc7ab0390824347940ecf083775 removed unused YXML_Find_Theorems and Legacy_XML_Syntax; diff -r 71e938856a03 -r 6415d95bf7a2 src/Pure/ROOT --- a/src/Pure/ROOT Thu Aug 08 23:34:52 2013 +0200 +++ b/src/Pure/ROOT Thu Aug 08 23:52:35 2013 +0200 @@ -201,7 +201,6 @@ "Thy/thy_output.ML" "Thy/thy_syntax.ML" "Tools/build.ML" - "Tools/legacy_xml_syntax.ML" "Tools/named_thms.ML" "Tools/proof_general.ML" "assumption.ML" diff -r 71e938856a03 -r 6415d95bf7a2 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Thu Aug 08 23:34:52 2013 +0200 +++ b/src/Pure/ROOT.ML Thu Aug 08 23:52:35 2013 +0200 @@ -302,7 +302,6 @@ use "Tools/build.ML"; use "Tools/named_thms.ML"; use "Tools/proof_general.ML"; -use "Tools/legacy_xml_syntax.ML"; (* ML toplevel pretty printing *) diff -r 71e938856a03 -r 6415d95bf7a2 src/Pure/Tools/find_theorems.ML --- a/src/Pure/Tools/find_theorems.ML Thu Aug 08 23:34:52 2013 +0200 +++ b/src/Pure/Tools/find_theorems.ML Thu Aug 08 23:52:35 2013 +0200 @@ -23,11 +23,6 @@ val read_criterion: Proof.context -> string criterion -> term criterion val read_query: Position.T -> string -> (bool * string criterion) list - val xml_of_query: term query -> XML.tree - val query_of_xml: XML.tree -> term query - val xml_of_result: int option * theorem list -> XML.tree - val result_of_xml: XML.tree -> int option * theorem list - val find_theorems: Proof.context -> thm option -> int option -> bool -> (bool * term criterion) list -> int option * (Facts.ref * thm) list val find_theorems_cmd: Proof.context -> thm option -> int option -> bool -> @@ -40,7 +35,6 @@ val pretty_theorem: Proof.context -> theorem -> Pretty.T val pretty_thm: Proof.context -> Facts.ref * thm -> Pretty.T - end; structure Find_Theorems: FIND_THEOREMS = @@ -108,46 +102,6 @@ fun map_criteria f {goal, limit, rem_dups, criteria} = {goal = goal, limit = limit, rem_dups = rem_dups, criteria = f criteria}; -fun xml_of_criterion (Name name) = XML.Elem (("Name", [("val", name)]), []) - | xml_of_criterion Intro = XML.Elem (("Intro", []) , []) - | 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", []), [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 (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 - val properties = [] - |> (if rem_dups then cons ("rem_dups", "") else I) - |> (if is_some limit then cons ("limit", Markup.print_int (the limit)) else I); - in - XML.Elem (("Query", properties), XML.Encode.list - (XML.Encode.pair XML.Encode.bool (single o xml_of_criterion)) criteria) - end - | xml_of_query _ = raise Fail "cannot serialize goal"; - -fun query_of_xml (XML.Elem (("Query", properties), body)) = - let - val rem_dups = Properties.defined properties "rem_dups"; - val limit = Properties.get properties "limit" |> Option.map Markup.parse_int; - val criteria = - XML.Decode.list (XML.Decode.pair XML.Decode.bool - (criterion_of_xml o the_single)) body; - in - {goal = NONE, limit = limit, rem_dups = rem_dups, criteria = criteria} - end - | query_of_xml tree = raise Legacy_XML_Syntax.XML ("query_of_xml: bad tree", tree); - (** theorems, either internal or external (without proof) **) @@ -162,35 +116,6 @@ Position.markup pos o Markup.properties [("name", name)] | fact_ref_markup fact_ref = raise Fail "bad fact ref"; -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", []), [Legacy_XML_Syntax.xml_of_term prop]); - -fun theorem_of_xml (XML.Elem (("External", properties), [tree])) = - let - val name = the (Properties.get properties "name"); - val pos = Position.of_properties properties; - val intvs_opt = - Option.map (single o Facts.Single o Markup.parse_int) - (Properties.get properties "index"); - in - External (Facts.Named ((name, pos), intvs_opt), Legacy_XML_Syntax.term_of_xml tree) - end - | theorem_of_xml tree = raise Legacy_XML_Syntax.XML ("theorem_of_xml: bad tree", tree); - -fun xml_of_result (opt_found, theorems) = - let - val properties = - if is_some opt_found then [("found", Markup.print_int (the opt_found))] else []; - in - XML.Elem (("Result", properties), XML.Encode.list (single o xml_of_theorem) theorems) - end; - -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 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; diff -r 71e938856a03 -r 6415d95bf7a2 src/Pure/Tools/isabelle.xsd --- a/src/Pure/Tools/isabelle.xsd Thu Aug 08 23:34:52 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,193 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff -r 71e938856a03 -r 6415d95bf7a2 src/Pure/Tools/legacy_xml_syntax.ML --- a/src/Pure/Tools/legacy_xml_syntax.ML Thu Aug 08 23:34:52 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,173 +0,0 @@ -(* 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 - ("\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; diff -r 71e938856a03 -r 6415d95bf7a2 src/Tools/WWW_Find/Start_WWW_Find.thy --- a/src/Tools/WWW_Find/Start_WWW_Find.thy Thu Aug 08 23:34:52 2013 +0200 +++ b/src/Tools/WWW_Find/Start_WWW_Find.thy Thu Aug 08 23:52:35 2013 +0200 @@ -5,7 +5,6 @@ theory Start_WWW_Find imports WWW_Find begin ML {* - YXML_Find_Theorems.init (); val port = Markup.parse_int (getenv "SCGIPORT"); ScgiServer.server' 10 "/" port; *} diff -r 71e938856a03 -r 6415d95bf7a2 src/Tools/WWW_Find/WWW_Find.thy --- a/src/Tools/WWW_Find/WWW_Find.thy Thu Aug 08 23:34:52 2013 +0200 +++ b/src/Tools/WWW_Find/WWW_Find.thy Thu Aug 08 23:52:35 2013 +0200 @@ -14,7 +14,6 @@ ML_file "echo.ML" ML_file "html_templates.ML" ML_file "find_theorems.ML" -ML_file "yxml_find_theorems.ML" end diff -r 71e938856a03 -r 6415d95bf7a2 src/Tools/WWW_Find/yxml_find_theorems.ML --- a/src/Tools/WWW_Find/yxml_find_theorems.ML Thu Aug 08 23:34:52 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,47 +0,0 @@ -(* Title: Tools/WWW_Find/yxml_find_theorems.ML - Author: Sree Harsha Totakura, TUM - Author: Lars Noschinski, TUM - Author: Alexander Krauss, TUM - -Simple find theorems web service with yxml interface for programmatic -invocation. -*) - -signature YXML_FIND_THEOREMS = -sig - val init: unit -> unit -end - - -structure YXML_Find_Theorems : YXML_FIND_THEOREMS = -struct - -val the_theory = "Main"; (* FIXME!!! EXPERIMENTAL *) - -fun yxml_find_theorems theorem_list yxml_query = - let - val ctxt = Proof_Context.init_global (Thy_Info.get_theory the_theory); - in - Find_Theorems.query_of_xml (YXML.parse yxml_query) - |> Find_Theorems.filter_theorems ctxt theorem_list - ||> rev o (filter (fn Find_Theorems.External x => true | _ => false)) - |> Find_Theorems.xml_of_result |> YXML.string_of - end; - -fun visible_facts facts = - Facts.dest_static [] facts - |> filter_out (Facts.is_concealed facts o #1); - -fun init () = - let - val all_facts = - maps Facts.selections - (visible_facts (Global_Theory.facts_of (Thy_Info.get_theory the_theory))) - |> map (Find_Theorems.External o apsnd prop_of); - in - ScgiServer.register ("yxml_find_theorems", SOME Mime.html (*FIXME?*), - ScgiServer.raw_post_handler (yxml_find_theorems all_facts)) - end; - -end; -