open Printf
-let pp_request (req: Http_types.request) =
- match req#path with
- | "/elim" -> "Elim"
- | "/match" -> "Match"
- | "/hint" -> "Hint"
- | "/locate" -> "Locate"
- | _ -> assert false
-
let pp_error title msg =
- sprintf "<hr size='1' /><div><b class='error'>%s:</b> %s</div>" title msg
+ sprintf "<div><b class='error'>%s:</b> %s</div><br />" title msg
let paginate ~size ~page l =
let min = 1 + (page-1) * size in
aux 1 l
(** pretty print a list of URIs to an HELM theory file *)
-let theory_of_result (req: Http_types.request) page result =
+let theory_of_result page result =
let results_per_page =
Helm_registry.get_int "search_engine.results_per_page"
in
let results_no = List.length result in
+ let buffer = Buffer.create (200 * results_no) in
let result = paginate ~size:results_per_page ~page result in
- let query_kind = pp_request req in
- let template query_kind summary results =
- sprintf
- "<!-- MOZILLA SEARCH PLUGIN: BEGIN LIST -->
- <div class='resultsbar'>
- <table width='100%%'>
- <tr>
- <td class='left'><b class='query_kind'>%s</b></td>
- <td class='right'>%s</td>
- </tr>
- </table>
- </div>
- <br />
- <div>
- %s
- </div>
- <!-- MOZILLA SEARCH PLUGIN: END LIST -->"
- query_kind summary results
- in
if results_no > 0 then
let mode = "typeonly" in
- let results =
- let idx = ref ((page - 1) * results_per_page + List.length result + 1) in
- List.fold_right
- (fun uri i ->
- decr idx ;
- sprintf
- "<tr>
- <td valign=\"top\">%d.</td>
- <td><span class=\"uri\">%s</span></td>
- </tr>
- <tr>
- <td />
- <td><ht:OBJECT uri=\"%s\" mode=\"%s\"/></td>
- </tr>%s"
- !idx uri uri mode i)
- result ""
+ let output_results () =
+ let idx = ref ((page - 1) * results_per_page) in
+ List.iter
+ (fun uri ->
+ incr idx;
+ Printf.bprintf buffer
+ "<tr>
+ <td valign=\"top\">%d.</td>
+ <td><span class=\"uri\">%s</span></td>
+ </tr>
+ <tr>
+ <td />
+ <td><ht:OBJECT uri=\"%s\" mode=\"%s\"/></td>
+ </tr>"
+ !idx uri uri mode) result ;
+ in
+ let summary =
+ sprintf "<b>%d</b> result%s found"
+ results_no (if results_no > 1 then "s" else "")
in
- template query_kind
- (sprintf "<b>%d</b> result%s found"
- results_no (if results_no > 1 then "s" else ""))
- (sprintf
- "<table xmlns:ht=\"http://www.cs.unibo.it/helm/namespaces/helm-theory\">
- %s
- </table>"
- results)
+ begin
+ Buffer.add_string buffer
+ "<table xmlns:ht=\"http://www.cs.unibo.it/helm/namespaces/helm-theory\">";
+ output_results ();
+ Buffer.add_string buffer "</table>";
+ (summary, Buffer.contents buffer)
+ end
else
- template query_kind "no results found" ""
+ ("no results found", "")
let html_of_interpretations interps =
- let radio_button n =
- sprintf "<input type=\"radio\" name=\"param.interp\" value=\"%d\" />" n
- in
- let text interp =
- String.concat "<br />"
- (List.map
- (fun (id, value) -> sprintf "<span>%s = %s</span>" id value)
- interp)
- in
- let rec aux n = function
- | [] -> []
- | interp::tl -> ((radio_button n)^(text interp))::(aux (n+1) tl)
+ let choice_of_interp interp =
+ sprintf "<table>\n%s\n</table>"
+ (String.concat "\n"
+ (List.map
+ (fun (k, v) ->
+ sprintf "<tr><td><em>%s</em></td><td>%s</td></tr>" k v)
+ interp))
in
- String.concat "<br />" (aux 0 interps)
+ let interp_no = ref ~-1 in
+ sprintf "<table class=\"interp\">\n%s\n</table>"
+ (String.concat "\n"
+ (List.map
+ (fun interp ->
+ sprintf "
+ <tr class=\"interp\">
+ <td><input type=\"radio\" name=\"param.interp\" value=\"%d\" /></td>
+ <td>
+ %s
+ </td></tr>"
+ (incr interp_no; !interp_no)
+ (choice_of_interp interp))
+ interps))