src/Tools/WWW_Find/find_theorems.ML
author wenzelm
Sun May 12 20:25:45 2013 +0200 (2013-05-12 ago)
changeset 51949 f6858bb224c9
parent 43074 8b566f0d226c
child 52855 fb1f026c48ff
permissions -rw-r--r--
some system options as context-sensitive config options;
     1 (*  Title:      Tools/WWW_Find/find_theorems.ML
     2     Author:     Timothy Bourke, NICTA
     3 
     4 Simple find_theorems server.
     5 *)
     6 
     7 local
     8 
     9 val default_limit = 20;
    10 val all_thy_names = sort string_ord (Thy_Info.get_names ());
    11 
    12 fun app_index f xs = fold_index (fn x => K (f x)) xs ();
    13 
    14 fun find_theorems arg_data send =
    15   let
    16     val args = Symtab.lookup arg_data;
    17 
    18     val query_str = the_default "" (args "query");
    19     fun get_query () =
    20       (query_str ^ ";")
    21       |> Outer_Syntax.scan Position.start
    22       |> filter Token.is_proper
    23       |> Scan.error Find_Theorems.query_parser
    24       |> fst;
    25 
    26     val limit = case args "limit" of
    27         NONE => default_limit
    28       | SOME str => the_default default_limit (Int.fromString str);
    29     val thy_name = the_default "Main" (args "theory");
    30     val with_dups = is_some (args "with_dups");
    31     
    32     val ctxt = Proof_Context.init_global (Thy_Info.get_theory thy_name);
    33 
    34     fun do_find query =
    35       let
    36         val (othmslen, thms) =
    37           Find_Theorems.find_theorems_cmd ctxt NONE (SOME limit) with_dups query
    38           ||> rev;
    39       in
    40         Xhtml.write send
    41           (HTML_Templates.find_theorems_summary (othmslen, length thms, arg_data));
    42         if null thms then ()
    43         else Xhtml.write_enclosed send HTML_Templates.find_theorems_table (fn send =>
    44                HTML_Unicode.print_mode (app_index (Xhtml.write send o HTML_Templates.html_thm ctxt)) thms)
    45       end;
    46   in
    47     send Xhtml.doctype_xhtml1_0_strict;
    48     Xhtml.write_enclosed send
    49       (HTML_Templates.header thy_name (args "query", limit, with_dups, all_thy_names))
    50       (fn send => 
    51         if query_str = "" then ()
    52         else
    53           do_find (get_query ())
    54           handle ERROR msg => Xhtml.write send (HTML_Templates.error msg))
    55   end;
    56 in
    57 
    58 val () = ScgiServer.register ("find_theorems", SOME Mime.html, ScgiServer.simple_handler find_theorems);
    59 
    60 end;
    61