removed unused YXML_Find_Theorems and Legacy_XML_Syntax;
authorwenzelm
Thu Aug 08 23:52:35 2013 +0200 (2013-08-08)
changeset 529266415d95bf7a2
parent 52925 71e938856a03
child 52927 9c6aef15a7ad
removed unused YXML_Find_Theorems and Legacy_XML_Syntax;
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/Tools/find_theorems.ML
src/Pure/Tools/isabelle.xsd
src/Pure/Tools/legacy_xml_syntax.ML
src/Tools/WWW_Find/Start_WWW_Find.thy
src/Tools/WWW_Find/WWW_Find.thy
src/Tools/WWW_Find/yxml_find_theorems.ML
     1.1 --- a/src/Pure/ROOT	Thu Aug 08 23:34:52 2013 +0200
     1.2 +++ b/src/Pure/ROOT	Thu Aug 08 23:52:35 2013 +0200
     1.3 @@ -201,7 +201,6 @@
     1.4      "Thy/thy_output.ML"
     1.5      "Thy/thy_syntax.ML"
     1.6      "Tools/build.ML"
     1.7 -    "Tools/legacy_xml_syntax.ML"
     1.8      "Tools/named_thms.ML"
     1.9      "Tools/proof_general.ML"
    1.10      "assumption.ML"
     2.1 --- a/src/Pure/ROOT.ML	Thu Aug 08 23:34:52 2013 +0200
     2.2 +++ b/src/Pure/ROOT.ML	Thu Aug 08 23:52:35 2013 +0200
     2.3 @@ -302,7 +302,6 @@
     2.4  use "Tools/build.ML";
     2.5  use "Tools/named_thms.ML";
     2.6  use "Tools/proof_general.ML";
     2.7 -use "Tools/legacy_xml_syntax.ML";
     2.8  
     2.9  
    2.10  (* ML toplevel pretty printing *)
     3.1 --- a/src/Pure/Tools/find_theorems.ML	Thu Aug 08 23:34:52 2013 +0200
     3.2 +++ b/src/Pure/Tools/find_theorems.ML	Thu Aug 08 23:52:35 2013 +0200
     3.3 @@ -23,11 +23,6 @@
     3.4    val read_criterion: Proof.context -> string criterion -> term criterion
     3.5    val read_query: Position.T -> string -> (bool * string criterion) list
     3.6  
     3.7 -  val xml_of_query: term query -> XML.tree
     3.8 -  val query_of_xml: XML.tree -> term query
     3.9 -  val xml_of_result: int option * theorem list -> XML.tree
    3.10 -  val result_of_xml: XML.tree -> int option * theorem list
    3.11 -
    3.12    val find_theorems: Proof.context -> thm option -> int option -> bool ->
    3.13      (bool * term criterion) list -> int option * (Facts.ref * thm) list
    3.14    val find_theorems_cmd: Proof.context -> thm option -> int option -> bool ->
    3.15 @@ -40,7 +35,6 @@
    3.16  
    3.17    val pretty_theorem: Proof.context -> theorem -> Pretty.T
    3.18    val pretty_thm: Proof.context -> Facts.ref * thm -> Pretty.T
    3.19 -
    3.20  end;
    3.21  
    3.22  structure Find_Theorems: FIND_THEOREMS =
    3.23 @@ -108,46 +102,6 @@
    3.24  fun map_criteria f {goal, limit, rem_dups, criteria} =
    3.25    {goal = goal, limit = limit, rem_dups = rem_dups, criteria = f criteria};
    3.26  
    3.27 -fun xml_of_criterion (Name name) = XML.Elem (("Name", [("val", name)]), [])
    3.28 -  | xml_of_criterion Intro = XML.Elem (("Intro", []) , [])
    3.29 -  | xml_of_criterion Elim = XML.Elem (("Elim", []) , [])
    3.30 -  | xml_of_criterion Dest = XML.Elem (("Dest", []) , [])
    3.31 -  | xml_of_criterion Solves = XML.Elem (("Solves", []) , [])
    3.32 -  | xml_of_criterion (Simp pat) = XML.Elem (("Simp", []), [Legacy_XML_Syntax.xml_of_term pat])
    3.33 -  | xml_of_criterion (Pattern pat) = XML.Elem (("Pattern", []), [Legacy_XML_Syntax.xml_of_term pat]);
    3.34 -
    3.35 -fun criterion_of_xml (XML.Elem (("Name", [("val", name)]), [])) = Name name
    3.36 -  | criterion_of_xml (XML.Elem (("Intro", []) , [])) = Intro
    3.37 -  | criterion_of_xml (XML.Elem (("Elim", []) , [])) = Elim
    3.38 -  | criterion_of_xml (XML.Elem (("Dest", []) , [])) = Dest
    3.39 -  | criterion_of_xml (XML.Elem (("Solves", []) , [])) = Solves
    3.40 -  | criterion_of_xml (XML.Elem (("Simp", []), [tree])) = Simp (Legacy_XML_Syntax.term_of_xml tree)
    3.41 -  | criterion_of_xml (XML.Elem (("Pattern", []), [tree])) = Pattern (Legacy_XML_Syntax.term_of_xml tree)
    3.42 -  | criterion_of_xml tree = raise Legacy_XML_Syntax.XML ("criterion_of_xml: bad tree", tree);
    3.43 -
    3.44 -fun xml_of_query {goal = NONE, limit, rem_dups, criteria} =
    3.45 -      let
    3.46 -        val properties = []
    3.47 -          |> (if rem_dups then cons ("rem_dups", "") else I)
    3.48 -          |> (if is_some limit then cons ("limit", Markup.print_int (the limit)) else I);
    3.49 -      in
    3.50 -        XML.Elem (("Query", properties), XML.Encode.list
    3.51 -          (XML.Encode.pair XML.Encode.bool (single o xml_of_criterion)) criteria)
    3.52 -      end
    3.53 -  | xml_of_query _ = raise Fail "cannot serialize goal";
    3.54 -
    3.55 -fun query_of_xml (XML.Elem (("Query", properties), body)) =
    3.56 -      let
    3.57 -        val rem_dups = Properties.defined properties "rem_dups";
    3.58 -        val limit = Properties.get properties "limit" |> Option.map Markup.parse_int;
    3.59 -        val criteria =
    3.60 -          XML.Decode.list (XML.Decode.pair XML.Decode.bool
    3.61 -            (criterion_of_xml o the_single)) body;
    3.62 -      in
    3.63 -        {goal = NONE, limit = limit, rem_dups = rem_dups, criteria = criteria}
    3.64 -      end
    3.65 -  | query_of_xml tree = raise Legacy_XML_Syntax.XML ("query_of_xml: bad tree", tree);
    3.66 -
    3.67  
    3.68  
    3.69  (** theorems, either internal or external (without proof) **)
    3.70 @@ -162,35 +116,6 @@
    3.71        Position.markup pos o Markup.properties [("name", name)]
    3.72    | fact_ref_markup fact_ref = raise Fail "bad fact ref";
    3.73  
    3.74 -fun xml_of_theorem (Internal _) = raise Fail "xml_of_theorem: Internal"
    3.75 -  | xml_of_theorem (External (fact_ref, prop)) =
    3.76 -      XML.Elem (fact_ref_markup fact_ref ("External", []), [Legacy_XML_Syntax.xml_of_term prop]);
    3.77 -
    3.78 -fun theorem_of_xml (XML.Elem (("External", properties), [tree])) =
    3.79 -      let
    3.80 -        val name = the (Properties.get properties "name");
    3.81 -        val pos = Position.of_properties properties;
    3.82 -        val intvs_opt =
    3.83 -          Option.map (single o Facts.Single o Markup.parse_int)
    3.84 -            (Properties.get properties "index");
    3.85 -      in
    3.86 -        External (Facts.Named ((name, pos), intvs_opt), Legacy_XML_Syntax.term_of_xml tree)
    3.87 -      end
    3.88 -  | theorem_of_xml tree = raise Legacy_XML_Syntax.XML ("theorem_of_xml: bad tree", tree);
    3.89 -
    3.90 -fun xml_of_result (opt_found, theorems) =
    3.91 -  let
    3.92 -    val properties =
    3.93 -      if is_some opt_found then [("found", Markup.print_int (the opt_found))] else [];
    3.94 -  in
    3.95 -    XML.Elem (("Result", properties), XML.Encode.list (single o xml_of_theorem) theorems)
    3.96 -  end;
    3.97 -
    3.98 -fun result_of_xml (XML.Elem (("Result", properties), body)) =
    3.99 -      (Properties.get properties "found" |> Option.map Markup.parse_int,
   3.100 -       XML.Decode.list (theorem_of_xml o the_single) body)
   3.101 -  | result_of_xml tree = raise Legacy_XML_Syntax.XML ("result_of_xml: bad tree", tree);
   3.102 -
   3.103  fun prop_of (Internal (_, thm)) = Thm.full_prop_of thm
   3.104    | prop_of (External (_, prop)) = prop;
   3.105  
     4.1 --- a/src/Pure/Tools/isabelle.xsd	Thu Aug 08 23:34:52 2013 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,193 +0,0 @@
     4.4 -<xsd:schema xmlns:xsd="http://www.w3.org/2001/XMLSchema">
     4.5 -
     4.6 -<xsd:element name="class">
     4.7 -  <xsd:complexType>
     4.8 -    <xsd:attribute name="name" type="xsd:string" use="required"/>
     4.9 -  </xsd:complexType>
    4.10 -</xsd:element>
    4.11 -
    4.12 -<xsd:element name="type">
    4.13 -  <xsd:complexType>
    4.14 -    <xsd:group ref="typeGroup"/>
    4.15 -  </xsd:complexType>
    4.16 -</xsd:element>
    4.17 -
    4.18 -<xsd:element name="types">
    4.19 -  <xsd:complexType>
    4.20 -    <xsd:group ref="typeGroup" minOccurs="0" maxOccurs="unbounded"/>
    4.21 -  </xsd:complexType>
    4.22 -</xsd:element>
    4.23 -
    4.24 -<xsd:group name="typeGroup">
    4.25 -  <xsd:choice>
    4.26 -    <xsd:element name="TVar">
    4.27 -      <xsd:complexType>
    4.28 -        <xsd:sequence>
    4.29 -          <xsd:element ref="class" minOccurs="0" maxOccurs="unbounded"/>
    4.30 -        </xsd:sequence>
    4.31 -        <xsd:attribute name="name" type="xsd:string" use="required"/>
    4.32 -        <xsd:attribute name="index" type="xsd:integer"/>
    4.33 -      </xsd:complexType>
    4.34 -    </xsd:element>
    4.35 -    <xsd:element name="TFree">
    4.36 -      <xsd:complexType>
    4.37 -        <xsd:sequence>
    4.38 -          <xsd:element ref="class" minOccurs="0" maxOccurs="unbounded"/>
    4.39 -        </xsd:sequence>
    4.40 -        <xsd:attribute name="name" type="xsd:string" use="required"/>
    4.41 -      </xsd:complexType>
    4.42 -    </xsd:element>
    4.43 -    <xsd:element name="Type">
    4.44 -      <xsd:complexType>
    4.45 -        <xsd:sequence>
    4.46 -          <xsd:group ref="typeGroup" minOccurs="0" maxOccurs="unbounded"/>
    4.47 -        </xsd:sequence>
    4.48 -        <xsd:attribute name="name" type="xsd:string" use="required"/>
    4.49 -      </xsd:complexType>
    4.50 -    </xsd:element>
    4.51 -  </xsd:choice>
    4.52 -</xsd:group>
    4.53 -
    4.54 -<xsd:element name="term">
    4.55 -  <xsd:complexType>
    4.56 -    <xsd:group ref="termGroup"/>
    4.57 -  </xsd:complexType>
    4.58 -</xsd:element>
    4.59 -
    4.60 -<xsd:group name="termGroup">
    4.61 -  <xsd:choice>
    4.62 -    <xsd:element name="Var">
    4.63 -      <xsd:complexType>
    4.64 -        <xsd:sequence>
    4.65 -          <xsd:group ref="typeGroup"/>
    4.66 -        </xsd:sequence>
    4.67 -        <xsd:attribute name="name" type="xsd:string" use="required"/>
    4.68 -        <xsd:attribute name="index" type="xsd:integer"/>
    4.69 -      </xsd:complexType>
    4.70 -    </xsd:element>
    4.71 -    <xsd:element name="Free">
    4.72 -      <xsd:complexType>
    4.73 -        <xsd:sequence>
    4.74 -          <xsd:group ref="typeGroup"/>
    4.75 -        </xsd:sequence>
    4.76 -        <xsd:attribute name="name" type="xsd:string" use="required"/>
    4.77 -      </xsd:complexType>
    4.78 -    </xsd:element>
    4.79 -    <xsd:element name="Const">
    4.80 -      <xsd:complexType>
    4.81 -        <xsd:sequence>
    4.82 -          <xsd:group ref="typeGroup"/>
    4.83 -        </xsd:sequence>
    4.84 -        <xsd:attribute name="name" type="xsd:string" use="required"/>
    4.85 -      </xsd:complexType>
    4.86 -    </xsd:element>
    4.87 -    <xsd:element name="Bound">
    4.88 -      <xsd:complexType>
    4.89 -        <xsd:attribute name="index" type="xsd:integer" use="required"/>
    4.90 -      </xsd:complexType>
    4.91 -    </xsd:element>
    4.92 -    <xsd:element name="App">
    4.93 -      <xsd:complexType>
    4.94 -        <xsd:sequence>
    4.95 -          <xsd:group ref="termGroup"/>
    4.96 -          <xsd:group ref="termGroup"/>
    4.97 -        </xsd:sequence>
    4.98 -      </xsd:complexType>
    4.99 -    </xsd:element>
   4.100 -    <xsd:element name="Abs">
   4.101 -      <xsd:complexType>
   4.102 -        <xsd:sequence>
   4.103 -          <xsd:group ref="typeGroup"/>
   4.104 -          <xsd:group ref="termGroup"/>
   4.105 -        </xsd:sequence>
   4.106 -        <xsd:attribute name="vname" type="xsd:string" use="required"/>
   4.107 -      </xsd:complexType>
   4.108 -    </xsd:element>
   4.109 -  </xsd:choice>
   4.110 -</xsd:group>
   4.111 -
   4.112 -<xsd:element name="proof">
   4.113 -  <xsd:complexType>
   4.114 -    <xsd:group ref="proofGroup"/>
   4.115 -  </xsd:complexType>
   4.116 -</xsd:element>
   4.117 -
   4.118 -<xsd:group name="proofGroup">
   4.119 -  <xsd:choice>
   4.120 -    <xsd:element name="PThm">
   4.121 -      <xsd:complexType>
   4.122 -        <xsd:sequence>
   4.123 -          <xsd:group ref="termGroup" minOccurs="0"/>
   4.124 -          <xsd:element ref="types" minOccurs="0"/>
   4.125 -        </xsd:sequence>
   4.126 -        <xsd:attribute name="name" type="xsd:string" use="required"/>
   4.127 -      </xsd:complexType>
   4.128 -    </xsd:element>
   4.129 -    <xsd:element name="PAxm">
   4.130 -      <xsd:complexType>
   4.131 -        <xsd:sequence>
   4.132 -          <xsd:group ref="termGroup" minOccurs="0"/>
   4.133 -          <xsd:element ref="types" minOccurs="0"/>
   4.134 -        </xsd:sequence>
   4.135 -        <xsd:attribute name="name" type="xsd:string" use="required"/>
   4.136 -      </xsd:complexType>
   4.137 -    </xsd:element>
   4.138 -    <xsd:element name="Oracle">
   4.139 -      <xsd:complexType>
   4.140 -        <xsd:sequence>
   4.141 -          <xsd:group ref="termGroup"/>
   4.142 -          <xsd:element ref="types" minOccurs="0"/>
   4.143 -        </xsd:sequence>
   4.144 -        <xsd:attribute name="name" type="xsd:string" use="required"/>
   4.145 -      </xsd:complexType>
   4.146 -    </xsd:element>
   4.147 -    <xsd:element name="PBound">
   4.148 -      <xsd:complexType>
   4.149 -        <xsd:attribute name="index" type="xsd:integer" use="required"/>
   4.150 -      </xsd:complexType>
   4.151 -    </xsd:element>
   4.152 -    <xsd:element name="Appt">
   4.153 -      <xsd:complexType>
   4.154 -        <xsd:sequence>
   4.155 -          <xsd:group ref="proofGroup"/>
   4.156 -          <xsd:group ref="termGroup" minOccurs="0"/>
   4.157 -        </xsd:sequence>
   4.158 -      </xsd:complexType>
   4.159 -    </xsd:element>
   4.160 -    <xsd:element name="AppP">
   4.161 -      <xsd:complexType>
   4.162 -        <xsd:sequence>
   4.163 -          <xsd:group ref="proofGroup"/>
   4.164 -          <xsd:group ref="proofGroup"/>
   4.165 -        </xsd:sequence>
   4.166 -      </xsd:complexType>
   4.167 -    </xsd:element>
   4.168 -    <xsd:element name="Abst">
   4.169 -      <xsd:complexType>
   4.170 -        <xsd:sequence>
   4.171 -          <xsd:group ref="typeGroup" minOccurs="0"/>
   4.172 -          <xsd:group ref="proofGroup"/>
   4.173 -        </xsd:sequence>
   4.174 -        <xsd:attribute name="vname" type="xsd:string" use="required"/>
   4.175 -      </xsd:complexType>
   4.176 -    </xsd:element>
   4.177 -    <xsd:element name="AbsP">
   4.178 -      <xsd:complexType>
   4.179 -        <xsd:sequence>
   4.180 -          <xsd:group ref="termGroup" minOccurs="0"/>
   4.181 -          <xsd:group ref="proofGroup"/>
   4.182 -        </xsd:sequence>
   4.183 -        <xsd:attribute name="vname" type="xsd:string" use="required"/>
   4.184 -      </xsd:complexType>
   4.185 -    </xsd:element>
   4.186 -    <xsd:element name="Hyp">
   4.187 -      <xsd:complexType>
   4.188 -        <xsd:sequence>
   4.189 -          <xsd:group ref="termGroup"/>
   4.190 -        </xsd:sequence>
   4.191 -      </xsd:complexType>
   4.192 -    </xsd:element>
   4.193 -  </xsd:choice>
   4.194 -</xsd:group>
   4.195 -
   4.196 -</xsd:schema>
     5.1 --- a/src/Pure/Tools/legacy_xml_syntax.ML	Thu Aug 08 23:34:52 2013 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,173 +0,0 @@
     5.4 -(*  Title:      Pure/Tools/legacy_xml_syntax.ML
     5.5 -    Author:     Stefan Berghofer, TU Muenchen
     5.6 -
     5.7 -Input and output of types, terms, and proofs in XML format.
     5.8 -See isabelle.xsd for a description of the syntax.
     5.9 -
    5.10 -Legacy module, see Pure/term_xml.ML etc.
    5.11 -*)
    5.12 -
    5.13 -signature LEGACY_XML_SYNTAX =
    5.14 -sig
    5.15 -  val xml_of_type: typ -> XML.tree
    5.16 -  val xml_of_term: term -> XML.tree
    5.17 -  val xml_of_proof: Proofterm.proof -> XML.tree
    5.18 -  val write_to_file: Path.T -> string -> XML.tree -> unit
    5.19 -  exception XML of string * XML.tree
    5.20 -  val type_of_xml: XML.tree -> typ
    5.21 -  val term_of_xml: XML.tree -> term
    5.22 -  val proof_of_xml: XML.tree -> Proofterm.proof
    5.23 -end;
    5.24 -
    5.25 -structure Legacy_XML_Syntax : LEGACY_XML_SYNTAX =
    5.26 -struct
    5.27 -
    5.28 -(**** XML output ****)
    5.29 -
    5.30 -fun xml_of_class name = XML.Elem (("class", [("name", name)]), []);
    5.31 -
    5.32 -fun xml_of_type (TVar ((s, i), S)) =
    5.33 -      XML.Elem (("TVar", ("name", s) :: (if i=0 then [] else [("index", string_of_int i)])),
    5.34 -        map xml_of_class S)
    5.35 -  | xml_of_type (TFree (s, S)) =
    5.36 -      XML.Elem (("TFree", [("name", s)]), map xml_of_class S)
    5.37 -  | xml_of_type (Type (s, Ts)) =
    5.38 -      XML.Elem (("Type", [("name", s)]), map xml_of_type Ts);
    5.39 -
    5.40 -fun xml_of_term (Bound i) =
    5.41 -      XML.Elem (("Bound", [("index", string_of_int i)]), [])
    5.42 -  | xml_of_term (Free (s, T)) =
    5.43 -      XML.Elem (("Free", [("name", s)]), [xml_of_type T])
    5.44 -  | xml_of_term (Var ((s, i), T)) =
    5.45 -      XML.Elem (("Var", ("name", s) :: (if i=0 then [] else [("index", string_of_int i)])),
    5.46 -        [xml_of_type T])
    5.47 -  | xml_of_term (Const (s, T)) =
    5.48 -      XML.Elem (("Const", [("name", s)]), [xml_of_type T])
    5.49 -  | xml_of_term (t $ u) =
    5.50 -      XML.Elem (("App", []), [xml_of_term t, xml_of_term u])
    5.51 -  | xml_of_term (Abs (s, T, t)) =
    5.52 -      XML.Elem (("Abs", [("vname", s)]), [xml_of_type T, xml_of_term t]);
    5.53 -
    5.54 -fun xml_of_opttypes NONE = []
    5.55 -  | xml_of_opttypes (SOME Ts) = [XML.Elem (("types", []), map xml_of_type Ts)];
    5.56 -
    5.57 -(* FIXME: the t argument of PThm and PAxm is actually redundant, since *)
    5.58 -(* it can be looked up in the theorem database. Thus, it could be      *)
    5.59 -(* omitted from the xml representation.                                *)
    5.60 -
    5.61 -(* FIXME not exhaustive *)
    5.62 -fun xml_of_proof (PBound i) =
    5.63 -      XML.Elem (("PBound", [("index", string_of_int i)]), [])
    5.64 -  | xml_of_proof (Abst (s, optT, prf)) =
    5.65 -      XML.Elem (("Abst", [("vname", s)]),
    5.66 -        (case optT of NONE => [] | SOME T => [xml_of_type T]) @ [xml_of_proof prf])
    5.67 -  | xml_of_proof (AbsP (s, optt, prf)) =
    5.68 -      XML.Elem (("AbsP", [("vname", s)]),
    5.69 -        (case optt of NONE => [] | SOME t => [xml_of_term t]) @ [xml_of_proof prf])
    5.70 -  | xml_of_proof (prf % optt) =
    5.71 -      XML.Elem (("Appt", []),
    5.72 -        xml_of_proof prf :: (case optt of NONE => [] | SOME t => [xml_of_term t]))
    5.73 -  | xml_of_proof (prf %% prf') =
    5.74 -      XML.Elem (("AppP", []), [xml_of_proof prf, xml_of_proof prf'])
    5.75 -  | xml_of_proof (Hyp t) = XML.Elem (("Hyp", []), [xml_of_term t])
    5.76 -  | xml_of_proof (PThm (_, ((s, t, optTs), _))) =
    5.77 -      XML.Elem (("PThm", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
    5.78 -  | xml_of_proof (PAxm (s, t, optTs)) =
    5.79 -      XML.Elem (("PAxm", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
    5.80 -  | xml_of_proof (Oracle (s, t, optTs)) =
    5.81 -      XML.Elem (("Oracle", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
    5.82 -  | xml_of_proof MinProof =
    5.83 -      XML.Elem (("MinProof", []), []);
    5.84 -
    5.85 -
    5.86 -(* useful for checking the output against a schema file *)
    5.87 -
    5.88 -fun write_to_file path elname x =
    5.89 -  File.write path
    5.90 -    ("<?xml version=\"1.0\" encoding=\"UTF-8\"?>\n" ^
    5.91 -     XML.string_of (XML.Elem ((elname,
    5.92 -         [("xmlns:xsi", "http://www.w3.org/2001/XMLSchema-instance"),
    5.93 -          ("xsi:noNamespaceSchemaLocation", "isabelle.xsd")]),
    5.94 -       [x])));
    5.95 -
    5.96 -
    5.97 -
    5.98 -(**** XML input ****)
    5.99 -
   5.100 -exception XML of string * XML.tree;
   5.101 -
   5.102 -fun class_of_xml (XML.Elem (("class", [("name", name)]), [])) = name
   5.103 -  | class_of_xml tree = raise XML ("class_of_xml: bad tree", tree);
   5.104 -
   5.105 -fun index_of_string s tree idx =
   5.106 -  (case Int.fromString idx of
   5.107 -    NONE => raise XML (s ^ ": bad index", tree)
   5.108 -  | SOME i => i);
   5.109 -
   5.110 -fun type_of_xml (tree as XML.Elem (("TVar", atts), classes)) = TVar
   5.111 -      ((case Properties.get atts "name" of
   5.112 -          NONE => raise XML ("type_of_xml: name of TVar missing", tree)
   5.113 -        | SOME name => name,
   5.114 -        the_default 0 (Option.map (index_of_string "type_of_xml" tree)
   5.115 -          (Properties.get atts "index"))),
   5.116 -       map class_of_xml classes)
   5.117 -  | type_of_xml (XML.Elem (("TFree", [("name", s)]), classes)) =
   5.118 -      TFree (s, map class_of_xml classes)
   5.119 -  | type_of_xml (XML.Elem (("Type", [("name", s)]), types)) =
   5.120 -      Type (s, map type_of_xml types)
   5.121 -  | type_of_xml tree = raise XML ("type_of_xml: bad tree", tree);
   5.122 -
   5.123 -fun term_of_xml (tree as XML.Elem (("Bound", [("index", idx)]), [])) =
   5.124 -      Bound (index_of_string "bad variable index" tree idx)
   5.125 -  | term_of_xml (XML.Elem (("Free", [("name", s)]), [typ])) =
   5.126 -      Free (s, type_of_xml typ)
   5.127 -  | term_of_xml (tree as XML.Elem (("Var", atts), [typ])) = Var
   5.128 -      ((case Properties.get atts "name" of
   5.129 -          NONE => raise XML ("type_of_xml: name of Var missing", tree)
   5.130 -        | SOME name => name,
   5.131 -        the_default 0 (Option.map (index_of_string "term_of_xml" tree)
   5.132 -          (Properties.get atts "index"))),
   5.133 -       type_of_xml typ)
   5.134 -  | term_of_xml (XML.Elem (("Const", [("name", s)]), [typ])) =
   5.135 -      Const (s, type_of_xml typ)
   5.136 -  | term_of_xml (XML.Elem (("App", []), [term, term'])) =
   5.137 -      term_of_xml term $ term_of_xml term'
   5.138 -  | term_of_xml (XML.Elem (("Abs", [("vname", s)]), [typ, term])) =
   5.139 -      Abs (s, type_of_xml typ, term_of_xml term)
   5.140 -  | term_of_xml tree = raise XML ("term_of_xml: bad tree", tree);
   5.141 -
   5.142 -fun opttypes_of_xml [] = NONE
   5.143 -  | opttypes_of_xml [XML.Elem (("types", []), types)] =
   5.144 -      SOME (map type_of_xml types)
   5.145 -  | opttypes_of_xml (tree :: _) = raise XML ("opttypes_of_xml: bad tree", tree);
   5.146 -
   5.147 -fun proof_of_xml (tree as XML.Elem (("PBound", [("index", idx)]), [])) =
   5.148 -      PBound (index_of_string "proof_of_xml" tree idx)
   5.149 -  | proof_of_xml (XML.Elem (("Abst", [("vname", s)]), [proof])) =
   5.150 -      Abst (s, NONE, proof_of_xml proof)
   5.151 -  | proof_of_xml (XML.Elem (("Abst", [("vname", s)]), [typ, proof])) =
   5.152 -      Abst (s, SOME (type_of_xml typ), proof_of_xml proof)
   5.153 -  | proof_of_xml (XML.Elem (("AbsP", [("vname", s)]), [proof])) =
   5.154 -      AbsP (s, NONE, proof_of_xml proof)
   5.155 -  | proof_of_xml (XML.Elem (("AbsP", [("vname", s)]), [term, proof])) =
   5.156 -      AbsP (s, SOME (term_of_xml term), proof_of_xml proof)
   5.157 -  | proof_of_xml (XML.Elem (("Appt", []), [proof])) =
   5.158 -      proof_of_xml proof % NONE
   5.159 -  | proof_of_xml (XML.Elem (("Appt", []), [proof, term])) =
   5.160 -      proof_of_xml proof % SOME (term_of_xml term)
   5.161 -  | proof_of_xml (XML.Elem (("AppP", []), [proof, proof'])) =
   5.162 -      proof_of_xml proof %% proof_of_xml proof'
   5.163 -  | proof_of_xml (XML.Elem (("Hyp", []), [term])) =
   5.164 -      Hyp (term_of_xml term)
   5.165 -  | proof_of_xml (XML.Elem (("PThm", [("name", s)]), term :: opttypes)) =
   5.166 -      (* FIXME? *)
   5.167 -      PThm (serial (), ((s, term_of_xml term, opttypes_of_xml opttypes),
   5.168 -        Future.value (Proofterm.approximate_proof_body MinProof)))
   5.169 -  | proof_of_xml (XML.Elem (("PAxm", [("name", s)]), term :: opttypes)) =
   5.170 -      PAxm (s, term_of_xml term, opttypes_of_xml opttypes)
   5.171 -  | proof_of_xml (XML.Elem (("Oracle", [("name", s)]), term :: opttypes)) =
   5.172 -      Oracle (s, term_of_xml term, opttypes_of_xml opttypes)
   5.173 -  | proof_of_xml (XML.Elem (("MinProof", _), _)) = MinProof
   5.174 -  | proof_of_xml tree = raise XML ("proof_of_xml: bad tree", tree);
   5.175 -
   5.176 -end;
     6.1 --- a/src/Tools/WWW_Find/Start_WWW_Find.thy	Thu Aug 08 23:34:52 2013 +0200
     6.2 +++ b/src/Tools/WWW_Find/Start_WWW_Find.thy	Thu Aug 08 23:52:35 2013 +0200
     6.3 @@ -5,7 +5,6 @@
     6.4  theory Start_WWW_Find imports WWW_Find begin
     6.5  
     6.6  ML {*
     6.7 -  YXML_Find_Theorems.init ();
     6.8    val port = Markup.parse_int (getenv "SCGIPORT");
     6.9    ScgiServer.server' 10 "/" port;
    6.10  *}
     7.1 --- a/src/Tools/WWW_Find/WWW_Find.thy	Thu Aug 08 23:34:52 2013 +0200
     7.2 +++ b/src/Tools/WWW_Find/WWW_Find.thy	Thu Aug 08 23:52:35 2013 +0200
     7.3 @@ -14,7 +14,6 @@
     7.4  ML_file "echo.ML"
     7.5  ML_file "html_templates.ML"
     7.6  ML_file "find_theorems.ML"
     7.7 -ML_file "yxml_find_theorems.ML"
     7.8  
     7.9  end
    7.10  
     8.1 --- a/src/Tools/WWW_Find/yxml_find_theorems.ML	Thu Aug 08 23:34:52 2013 +0200
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,47 +0,0 @@
     8.4 -(*  Title:      Tools/WWW_Find/yxml_find_theorems.ML
     8.5 -    Author:     Sree Harsha Totakura, TUM
     8.6 -    Author:     Lars Noschinski, TUM
     8.7 -    Author:     Alexander Krauss, TUM
     8.8 -
     8.9 -Simple find theorems web service with yxml interface for programmatic
    8.10 -invocation.
    8.11 -*)
    8.12 -
    8.13 -signature YXML_FIND_THEOREMS =
    8.14 -sig
    8.15 -  val init: unit -> unit
    8.16 -end
    8.17 -
    8.18 -
    8.19 -structure YXML_Find_Theorems : YXML_FIND_THEOREMS =
    8.20 -struct
    8.21 -
    8.22 -val the_theory = "Main"; (* FIXME!!! EXPERIMENTAL *)
    8.23 -
    8.24 -fun yxml_find_theorems theorem_list yxml_query =
    8.25 -  let
    8.26 -    val ctxt = Proof_Context.init_global (Thy_Info.get_theory the_theory);
    8.27 -  in
    8.28 -    Find_Theorems.query_of_xml (YXML.parse yxml_query)
    8.29 -    |> Find_Theorems.filter_theorems ctxt theorem_list
    8.30 -    ||> rev o (filter (fn Find_Theorems.External x => true | _ => false))
    8.31 -    |> Find_Theorems.xml_of_result |> YXML.string_of
    8.32 -  end;
    8.33 -
    8.34 -fun visible_facts facts =
    8.35 -  Facts.dest_static [] facts
    8.36 -  |> filter_out (Facts.is_concealed facts o #1);
    8.37 -
    8.38 -fun init () =
    8.39 -  let
    8.40 -    val all_facts =
    8.41 -      maps Facts.selections
    8.42 -        (visible_facts (Global_Theory.facts_of (Thy_Info.get_theory the_theory)))
    8.43 -      |> map (Find_Theorems.External o apsnd prop_of);
    8.44 -  in
    8.45 -    ScgiServer.register ("yxml_find_theorems", SOME Mime.html (*FIXME?*),
    8.46 -      ScgiServer.raw_post_handler (yxml_find_theorems all_facts))
    8.47 -  end;
    8.48 -
    8.49 -end;
    8.50 -