5 *) |
5 *) |
6 |
6 |
7 local |
7 local |
8 |
8 |
9 val default_limit = 20; |
9 val default_limit = 20; |
10 val thy_names = sort string_ord (Thy_Info.get_names ()); |
10 val all_thy_names = sort string_ord (Thy_Info.get_names ()); |
11 |
|
12 val find_theorems_url = "find_theorems"; |
|
13 |
|
14 fun is_sorry thm = |
|
15 Thm.proof_of thm |
|
16 |> Proofterm.approximate_proof_body |
|
17 |> Proofterm.all_oracles_of |
|
18 |> exists (fn (x, _) => x = "Pure.skip_proof"); |
|
19 |
|
20 local open Xhtml in |
|
21 fun find_theorems_form thy_name (query, limit, withdups) = |
|
22 let |
|
23 val query_input = |
|
24 input (id "query", { |
|
25 name = "query", |
|
26 itype = TextInput { value = query, maxlength = NONE }}); |
|
27 |
|
28 val max_results = divele noid |
|
29 [ |
|
30 label (noid, { for = "limit" }, "Max. results:"), |
|
31 input (id "limit", |
|
32 { name = "limit", |
|
33 itype = TextInput { value = SOME (string_of_int limit), |
|
34 maxlength = NONE }}) |
|
35 ]; |
|
36 |
|
37 val theories = divele noid |
|
38 [ |
|
39 label (noid, { for = "theory" }, "Search in:"), |
|
40 select (id "theory", { name = "theory", value = SOME thy_name }) |
|
41 thy_names |
|
42 ]; |
|
43 |
|
44 val with_dups = divele noid |
|
45 [ |
|
46 label (noid, { for = "withdups" }, "Allow duplicates:"), |
|
47 input (id "withdups", |
|
48 { name = "withdups", |
|
49 itype = Checkbox { checked = withdups, value = SOME "true" }}) |
|
50 ]; |
|
51 |
|
52 val help = divele (class "help") |
|
53 [ a { href="/pasting_help.html", text="(pasting from proof general)" } ]; |
|
54 in |
|
55 form (id "findtheorems", { method = "post", action = "/isabelle/find_theorems" }) |
|
56 [tag "fieldset" [] |
|
57 [tag "legend" [] [text "find_theorems"], |
|
58 (add_script (OnKeyPress, "encodequery(this)") |
|
59 o add_script (OnChange, "encodequery(this)") |
|
60 o add_script (OnMouseUp, "encodequery(this)")) query_input, |
|
61 divele (class "settings") [ max_results, theories, with_dups, help ], |
|
62 divele (class "mainbuttons") |
|
63 [ reset_button (id "reset"), submit_button (id "submit") ] |
|
64 ] |
|
65 ] |
|
66 end; |
|
67 |
|
68 fun html_header thy_name args = |
|
69 html { lang = "en" } [ |
|
70 head { title = "Find Theorems: results", stylesheet_href = "/basic.css" } |
|
71 [script (noid, { script_type="text/javascript", |
|
72 src="/find_theorems.js" })], |
|
73 add_script (OnLoad, "encodequery(document.getElementById('query'))") |
|
74 (body noid [ |
|
75 h (noid, 1, "Theory " ^ thy_name), |
|
76 find_theorems_form thy_name args, |
|
77 divele noid [] |
|
78 ]) |
|
79 ]; |
|
80 |
|
81 fun html_error msg = p ((class "error"), msg); |
|
82 |
|
83 val find_theorems_table = |
|
84 table (class "findtheorems") |
|
85 [ |
|
86 thead noid [tr [th (noid, "name"), th (noid, "theorem")]], |
|
87 tbody noid [] |
|
88 ]; |
|
89 |
|
90 fun show_criterion (b, c) = |
|
91 let |
|
92 fun prfx s = let |
|
93 val (c, v) = if b then ("criterion", s) else ("ncriterion", "-" ^ s); |
|
94 in span (class c, v) end; |
|
95 in |
|
96 (case c of |
|
97 Find_Theorems.Name name => prfx ("name: " ^ quote name) |
|
98 | Find_Theorems.Intro => prfx "intro" |
|
99 | Find_Theorems.IntroIff => prfx "introiff" |
|
100 | Find_Theorems.Elim => prfx "elim" |
|
101 | Find_Theorems.Dest => prfx "dest" |
|
102 | Find_Theorems.Solves => prfx "solves" |
|
103 | Find_Theorems.Simp pat => prfx ("simp: \"" ^ pat ^ "\"") |
|
104 | Find_Theorems.Pattern pat => prfx ("\"" ^ pat ^ "\"")) |
|
105 end; |
|
106 |
|
107 fun find_theorems_summary (othmslen, thmslen, args) = |
|
108 let |
|
109 val args = |
|
110 (case othmslen of |
|
111 NONE => args |
|
112 | SOME l => Symtab.update ("limit", string_of_int l) args) |
|
113 val qargs = HttpUtil.make_query_string args; |
|
114 |
|
115 val num_found_text = |
|
116 (case othmslen of |
|
117 NONE => text (string_of_int thmslen) |
|
118 | SOME l => |
|
119 a { href = find_theorems_url ^ |
|
120 (if qargs = "" then "" else "?" ^ qargs), |
|
121 text = string_of_int l }) |
|
122 val found = [text "found ", num_found_text, text " theorems"] : tag list; |
|
123 val displayed = |
|
124 if is_some othmslen |
|
125 then " (" ^ string_of_int thmslen ^ " displayed)" |
|
126 else ""; |
|
127 in |
|
128 table (class "findtheoremsquery") |
|
129 [ tr [ th' noid (found @ [text (displayed ^ ":")]) ] ] |
|
130 end |
|
131 |
|
132 fun sorry_class thm = if is_sorry thm then class "sorried" else noid; |
|
133 |
|
134 fun html_thm ctxt (n, (thmref, thm)) = |
|
135 let |
|
136 val output_thm = |
|
137 Output.output o Pretty.string_of_margin 100 o |
|
138 Display.pretty_thm (Config.put show_question_marks false ctxt); |
|
139 in |
|
140 tag' "tr" (class ("row" ^ string_of_int (n mod 2))) |
|
141 [ |
|
142 tag' "td" (class "name") |
|
143 [span' (sorry_class thm) |
|
144 [raw_text (Facts.string_of_ref thmref)] |
|
145 ], |
|
146 tag' "td" (class "thm") [pre noid (output_thm thm)] |
|
147 ] |
|
148 end; |
|
149 |
|
150 end; |
|
151 |
11 |
152 fun app_index f xs = fold_index (fn x => K (f x)) xs (); |
12 fun app_index f xs = fold_index (fn x => K (f x)) xs (); |
153 |
13 |
154 fun parse_request (ScgiReq.Req {request_method, query_string, ...}, content, send) = |
14 fun parse_request (ScgiReq.Req {request_method, query_string, ...}, content, send) = |
155 (case request_method of |
15 (case request_method of |
186 val (othmslen, thms) = |
46 val (othmslen, thms) = |
187 Find_Theorems.find_theorems_cmd ctxt NONE (SOME limit) with_dups query |
47 Find_Theorems.find_theorems_cmd ctxt NONE (SOME limit) with_dups query |
188 ||> rev; |
48 ||> rev; |
189 in |
49 in |
190 Xhtml.write send |
50 Xhtml.write send |
191 (find_theorems_summary (othmslen, length thms, arg_data)); |
51 (HTML_Templates.find_theorems_summary (othmslen, length thms, arg_data)); |
192 if null thms then () |
52 if null thms then () |
193 else Xhtml.write_enclosed send find_theorems_table (fn send => |
53 else Xhtml.write_enclosed send HTML_Templates.find_theorems_table (fn send => |
194 HTML_Unicode.print_mode (app_index (Xhtml.write send o html_thm ctxt)) thms) |
54 HTML_Unicode.print_mode (app_index (Xhtml.write send o HTML_Templates.html_thm ctxt)) thms) |
195 end; |
55 end; |
196 in |
56 in |
197 send Xhtml.doctype_xhtml1_0_strict; |
57 send Xhtml.doctype_xhtml1_0_strict; |
198 Xhtml.write_enclosed send |
58 Xhtml.write_enclosed send |
199 (html_header thy_name (args "query", limit, with_dups)) |
59 (HTML_Templates.header thy_name (args "query", limit, with_dups, all_thy_names)) |
200 (fn send => |
60 (fn send => |
201 if query_str = "" then () |
61 if query_str = "" then () |
202 else |
62 else |
203 do_find (get_query ()) |
63 do_find (get_query ()) |
204 handle ERROR msg => Xhtml.write send (html_error msg)) |
64 handle ERROR msg => Xhtml.write send (HTML_Templates.error msg)) |
205 end; |
65 end; |
206 in |
66 in |
207 |
67 |
208 val () = Printer.show_question_marks_default := false; |
68 val () = Printer.show_question_marks_default := false; |
209 val () = ScgiServer.register (find_theorems_url, SOME Mime.html, find_theorems o parse_request); |
69 val () = ScgiServer.register ("find_theorems", SOME Mime.html, find_theorems o parse_request); |
210 |
70 |
211 end; |
71 end; |
212 |
72 |