src/Tools/WWW_Find/find_theorems.ML
author wenzelm
Sat, 09 Jul 2011 21:53:27 +0200
changeset 43721 fad8634cee62
parent 43074 8b566f0d226c
child 51949 f6858bb224c9
permissions -rw-r--r--
echo prover input via raw_messages, for improved protocol tracing;
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");
33817
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    19
    fun get_query () =
43072
8aeb7ec8003a attempt to clarify code; removed "handle _" and dead code
krauss
parents: 43068
diff changeset
    20
      (query_str ^ ";")
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36959
diff changeset
    21
      |> Outer_Syntax.scan Position.start
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36745
diff changeset
    22
      |> filter Token.is_proper
43068
ac769b5edd1d exported raw query parser; removed inconsistent clone
krauss
parents: 43067
diff changeset
    23
      |> Scan.error Find_Theorems.query_parser
33817
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    24
      |> fst;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    25
43072
8aeb7ec8003a attempt to clarify code; removed "handle _" and dead code
krauss
parents: 43068
diff changeset
    26
    val limit = case args "limit" of
8aeb7ec8003a attempt to clarify code; removed "handle _" and dead code
krauss
parents: 43068
diff changeset
    27
        NONE => default_limit
8aeb7ec8003a attempt to clarify code; removed "handle _" and dead code
krauss
parents: 43068
diff changeset
    28
      | SOME str => the_default default_limit (Int.fromString str);
8aeb7ec8003a attempt to clarify code; removed "handle _" and dead code
krauss
parents: 43068
diff changeset
    29
    val thy_name = the_default "Main" (args "theory");
33817
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    30
    val with_dups = is_some (args "with_dups");
43072
8aeb7ec8003a attempt to clarify code; removed "handle _" and dead code
krauss
parents: 43068
diff changeset
    31
    
8aeb7ec8003a attempt to clarify code; removed "handle _" and dead code
krauss
parents: 43068
diff changeset
    32
    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
    33
43072
8aeb7ec8003a attempt to clarify code; removed "handle _" and dead code
krauss
parents: 43068
diff changeset
    34
    fun do_find query =
33817
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    35
      let
43072
8aeb7ec8003a attempt to clarify code; removed "handle _" and dead code
krauss
parents: 43068
diff changeset
    36
        val (othmslen, thms) =
8aeb7ec8003a attempt to clarify code; removed "handle _" and dead code
krauss
parents: 43068
diff changeset
    37
          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
    38
          ||> rev;
33817
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    39
      in
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    40
        Xhtml.write send
43073
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents: 43072
diff changeset
    41
          (HTML_Templates.find_theorems_summary (othmslen, length thms, arg_data));
33817
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    42
        if null thms then ()
43073
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents: 43072
diff changeset
    43
        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
    44
               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
    45
      end;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    46
  in
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    47
    send Xhtml.doctype_xhtml1_0_strict;
43072
8aeb7ec8003a attempt to clarify code; removed "handle _" and dead code
krauss
parents: 43068
diff changeset
    48
    Xhtml.write_enclosed send
43073
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents: 43072
diff changeset
    49
      (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
    50
      (fn send => 
8aeb7ec8003a attempt to clarify code; removed "handle _" and dead code
krauss
parents: 43068
diff changeset
    51
        if query_str = "" then ()
8aeb7ec8003a attempt to clarify code; removed "handle _" and dead code
krauss
parents: 43068
diff changeset
    52
        else
8aeb7ec8003a attempt to clarify code; removed "handle _" and dead code
krauss
parents: 43068
diff changeset
    53
          do_find (get_query ())
43073
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents: 43072
diff changeset
    54
          handle ERROR msg => Xhtml.write send (HTML_Templates.error msg))
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
in
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 36960
diff changeset
    57
42289
dafae095d733 discontinued special status of structure Printer;
wenzelm
parents: 41522
diff changeset
    58
val () = Printer.show_question_marks_default := false;
43074
8b566f0d226c generic ScgiServer.simple_handler
krauss
parents: 43073
diff changeset
    59
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
    60
33817
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    61
end;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    62