author | wenzelm |
Thu, 10 Oct 2013 12:02:12 +0200 | |
changeset 54320 | b8bd31c7058c |
parent 52925 | 71e938856a03 |
permissions | -rw-r--r-- |
33823 | 1 |
(* Title: Tools/WWW_Find/find_theorems.ML |
33817 | 2 |
Author: Timothy Bourke, NICTA |
3 |
||
33823 | 4 |
Simple find_theorems server. |
33817 | 5 |
*) |
6 |
||
7 |
local |
|
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36960
diff
changeset
|
8 |
|
33817 | 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 | 11 |
|
12 |
fun app_index f xs = fold_index (fn x => K (f x)) xs (); |
|
13 |
||
43074 | 14 |
fun find_theorems arg_data send = |
33817 | 15 |
let |
16 |
val args = Symtab.lookup arg_data; |
|
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 | 19 |
fun get_query () = Find_Theorems.read_query Position.none query_str; |
33817 | 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 | 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 | 28 |
|
43072
8aeb7ec8003a
attempt to clarify code; removed "handle _" and dead code
krauss
parents:
43068
diff
changeset
|
29 |
fun do_find query = |
33817 | 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 | 34 |
in |
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 | 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 | 40 |
end; |
41 |
in |
|
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 | 50 |
end; |
51 |
in |
|
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36960
diff
changeset
|
52 |
|
43074 | 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 | 55 |
end; |
56 |