src/Tools/WWW_Find/find_theorems.ML
author wenzelm
Thu, 10 Oct 2013 12:02:12 +0200
changeset 54320 b8bd31c7058c
parent 52925 71e938856a03
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33823
24090eae50b6 standardized headers;
wenzelm
parents: 33817
diff changeset
     1
(*  Title:      Tools/WWW_Find/find_theorems.ML
33817
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
     2
    Author:     Timothy Bourke, NICTA
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
     3
33823
24090eae50b6 standardized headers;
wenzelm
parents: 33817
diff changeset
     4
Simple find_theorems server.
33817
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
     5
*)
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
     6
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
     7
local
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 36960
diff changeset
     8
33817
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
     9
val default_limit = 20;
43073
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents: 43072
diff changeset
    10
val all_thy_names = sort string_ord (Thy_Info.get_names ());
33817
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    11
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    12
fun app_index f xs = fold_index (fn x => K (f x)) xs ();
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    13
43074
8b566f0d226c generic ScgiServer.simple_handler
krauss
parents: 43073
diff changeset
    14
fun find_theorems arg_data send =
33817
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    15
  let
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    16
    val args = Symtab.lookup arg_data;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    17
43072
8aeb7ec8003a attempt to clarify code; removed "handle _" and dead code
krauss
parents: 43068
diff changeset
    18
    val query_str = the_default "" (args "query");
52925
71e938856a03 more robust read_query;
wenzelm
parents: 52855
diff changeset
    19
    fun get_query () = Find_Theorems.read_query Position.none query_str;
33817
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    20
43072
8aeb7ec8003a attempt to clarify code; removed "handle _" and dead code
krauss
parents: 43068
diff changeset
    21
    val limit = case args "limit" of
8aeb7ec8003a attempt to clarify code; removed "handle _" and dead code
krauss
parents: 43068
diff changeset
    22
        NONE => default_limit
8aeb7ec8003a attempt to clarify code; removed "handle _" and dead code
krauss
parents: 43068
diff changeset
    23
      | SOME str => the_default default_limit (Int.fromString str);
8aeb7ec8003a attempt to clarify code; removed "handle _" and dead code
krauss
parents: 43068
diff changeset
    24
    val thy_name = the_default "Main" (args "theory");
33817
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    25
    val with_dups = is_some (args "with_dups");
43072
8aeb7ec8003a attempt to clarify code; removed "handle _" and dead code
krauss
parents: 43068
diff changeset
    26
    
8aeb7ec8003a attempt to clarify code; removed "handle _" and dead code
krauss
parents: 43068
diff changeset
    27
    val ctxt = Proof_Context.init_global (Thy_Info.get_theory thy_name);
33817
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    28
43072
8aeb7ec8003a attempt to clarify code; removed "handle _" and dead code
krauss
parents: 43068
diff changeset
    29
    fun do_find query =
33817
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    30
      let
43072
8aeb7ec8003a attempt to clarify code; removed "handle _" and dead code
krauss
parents: 43068
diff changeset
    31
        val (othmslen, thms) =
8aeb7ec8003a attempt to clarify code; removed "handle _" and dead code
krauss
parents: 43068
diff changeset
    32
          Find_Theorems.find_theorems_cmd ctxt NONE (SOME limit) with_dups query
8aeb7ec8003a attempt to clarify code; removed "handle _" and dead code
krauss
parents: 43068
diff changeset
    33
          ||> rev;
33817
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    34
      in
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    35
        Xhtml.write send
43073
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents: 43072
diff changeset
    36
          (HTML_Templates.find_theorems_summary (othmslen, length thms, arg_data));
33817
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    37
        if null thms then ()
43073
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents: 43072
diff changeset
    38
        else Xhtml.write_enclosed send HTML_Templates.find_theorems_table (fn send =>
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents: 43072
diff changeset
    39
               HTML_Unicode.print_mode (app_index (Xhtml.write send o HTML_Templates.html_thm ctxt)) thms)
33817
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    40
      end;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    41
  in
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    42
    send Xhtml.doctype_xhtml1_0_strict;
43072
8aeb7ec8003a attempt to clarify code; removed "handle _" and dead code
krauss
parents: 43068
diff changeset
    43
    Xhtml.write_enclosed send
43073
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents: 43072
diff changeset
    44
      (HTML_Templates.header thy_name (args "query", limit, with_dups, all_thy_names))
43072
8aeb7ec8003a attempt to clarify code; removed "handle _" and dead code
krauss
parents: 43068
diff changeset
    45
      (fn send => 
8aeb7ec8003a attempt to clarify code; removed "handle _" and dead code
krauss
parents: 43068
diff changeset
    46
        if query_str = "" then ()
8aeb7ec8003a attempt to clarify code; removed "handle _" and dead code
krauss
parents: 43068
diff changeset
    47
        else
8aeb7ec8003a attempt to clarify code; removed "handle _" and dead code
krauss
parents: 43068
diff changeset
    48
          do_find (get_query ())
43073
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents: 43072
diff changeset
    49
          handle ERROR msg => Xhtml.write send (HTML_Templates.error msg))
33817
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    50
  end;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    51
in
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 36960
diff changeset
    52
43074
8b566f0d226c generic ScgiServer.simple_handler
krauss
parents: 43073
diff changeset
    53
val () = ScgiServer.register ("find_theorems", SOME Mime.html, ScgiServer.simple_handler find_theorems);
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 36960
diff changeset
    54
33817
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    55
end;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    56