(* Title: Tools/WWW_Find/find_theorems.ML
Author: Timothy Bourke, NICTA
Simple find_theorems server.
*)
local
val default_limit = 20;
val all_thy_names = sort string_ord (Thy_Info.get_names ());
fun app_index f xs = fold_index (fn x => K (f x)) xs ();
fun find_theorems arg_data send =
let
val args = Symtab.lookup arg_data;
val query_str = the_default "" (args "query");
fun get_query () =
(query_str ^ ";")
|> Outer_Syntax.scan Position.start
|> filter Token.is_proper
|> Scan.error Find_Theorems.query_parser
|> fst;
val limit = case args "limit" of
NONE => default_limit
| SOME str => the_default default_limit (Int.fromString str);
val thy_name = the_default "Main" (args "theory");
val with_dups = is_some (args "with_dups");
val ctxt = Proof_Context.init_global (Thy_Info.get_theory thy_name);
fun do_find query =
let
val (othmslen, thms) =
Find_Theorems.find_theorems_cmd ctxt NONE (SOME limit) with_dups query
||> rev;
in
Xhtml.write send
(HTML_Templates.find_theorems_summary (othmslen, length thms, arg_data));
if null thms then ()
else Xhtml.write_enclosed send HTML_Templates.find_theorems_table (fn send =>
HTML_Unicode.print_mode (app_index (Xhtml.write send o HTML_Templates.html_thm ctxt)) thms)
end;
in
send Xhtml.doctype_xhtml1_0_strict;
Xhtml.write_enclosed send
(HTML_Templates.header thy_name (args "query", limit, with_dups, all_thy_names))
(fn send =>
if query_str = "" then ()
else
do_find (get_query ())
handle ERROR msg => Xhtml.write send (HTML_Templates.error msg))
end;
in
val () = Printer.show_question_marks_default := false;
val () = ScgiServer.register ("find_theorems", SOME Mime.html, ScgiServer.simple_handler find_theorems);
end;