src/Tools/WWW_Find/yxml_find_theorems.ML

explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions;
tuned;

(*  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;