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