author | wenzelm |
Wed, 08 Jun 2011 14:44:54 +0200 | |
changeset 43275 | 327b91364464 |
parent 43075 | 6fde0c323c15 |
permissions | -rw-r--r-- |
43275 | 1 |
(* Title: Tools/WWW_Find/yxml_find_theorems.ML |
43075
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff
changeset
|
2 |
Author: Sree Harsha Totakura, TUM |
43275 | 3 |
Author: Lars Noschinski, TUM |
4 |
Author: Alexander Krauss, TUM |
|
43075
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff
changeset
|
5 |
|
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff
changeset
|
6 |
Simple find theorems web service with yxml interface for programmatic |
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff
changeset
|
7 |
invocation. |
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff
changeset
|
8 |
*) |
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff
changeset
|
9 |
|
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff
changeset
|
10 |
signature YXML_FIND_THEOREMS = |
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff
changeset
|
11 |
sig |
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff
changeset
|
12 |
val init: unit -> unit |
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff
changeset
|
13 |
end |
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff
changeset
|
14 |
|
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff
changeset
|
15 |
|
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff
changeset
|
16 |
structure YXML_Find_Theorems : YXML_FIND_THEOREMS = |
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff
changeset
|
17 |
struct |
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff
changeset
|
18 |
|
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff
changeset
|
19 |
val the_theory = "Main"; (* FIXME!!! EXPERIMENTAL *) |
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff
changeset
|
20 |
|
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff
changeset
|
21 |
fun yxml_find_theorems theorem_list yxml_query = |
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff
changeset
|
22 |
let |
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff
changeset
|
23 |
val ctxt = Proof_Context.init_global (Thy_Info.get_theory the_theory); |
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff
changeset
|
24 |
in |
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff
changeset
|
25 |
Find_Theorems.query_of_xml (YXML.parse yxml_query) |
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff
changeset
|
26 |
|> Find_Theorems.filter_theorems ctxt theorem_list |
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff
changeset
|
27 |
||> rev o (filter (fn Find_Theorems.External x => true | _ => false)) |
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff
changeset
|
28 |
|> Find_Theorems.xml_of_result |> YXML.string_of |
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff
changeset
|
29 |
end; |
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff
changeset
|
30 |
|
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff
changeset
|
31 |
fun visible_facts facts = |
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff
changeset
|
32 |
Facts.dest_static [] facts |
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff
changeset
|
33 |
|> filter_out (Facts.is_concealed facts o #1); |
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff
changeset
|
34 |
|
43275 | 35 |
fun init () = |
43075
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff
changeset
|
36 |
let |
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff
changeset
|
37 |
val all_facts = |
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff
changeset
|
38 |
maps Facts.selections |
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff
changeset
|
39 |
(visible_facts (Global_Theory.facts_of (Thy_Info.get_theory the_theory))) |
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff
changeset
|
40 |
|> map (Find_Theorems.External o apsnd prop_of); |
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff
changeset
|
41 |
in |
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff
changeset
|
42 |
ScgiServer.register ("yxml_find_theorems", SOME Mime.html (*FIXME?*), |
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff
changeset
|
43 |
ScgiServer.raw_post_handler (yxml_find_theorems all_facts)) |
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff
changeset
|
44 |
end; |
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff
changeset
|
45 |
|
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff
changeset
|
46 |
end; |
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff
changeset
|
47 |