]> matita.cs.unibo.it Git - helm.git/blob - helm/searchEngine/mooglePp.ml
uses auto_tac_new instead of auto_tac
[helm.git] / helm / searchEngine / mooglePp.ml
1
2 open Printf
3
4 let pp_error title msg =
5   sprintf "<div><b class='error'>%s:</b> %s</div><br />" title msg
6
7 let paginate ~size ~page l =
8   let min = 1 + (page-1) * size in
9   let max = page * size in
10   let rec aux i l =
11     match (i, l) with
12     | _, [] -> []
13     | i, hd :: tl when i < min -> aux (i+1) tl
14     | i, hd :: tl when i >= min && i <= max -> hd :: aux (i+1) tl
15     | i, hd :: tl -> []
16   in
17   assert (size > 0 && page > 0);
18   aux 1 l
19
20   (** pretty print a list of URIs to an HELM theory file *)
21 let theory_of_result page result =
22   let results_per_page =
23     Helm_registry.get_int "search_engine.results_per_page"
24   in
25   let results_no = List.length result in
26   let result = paginate ~size:results_per_page ~page result in
27   if results_no > 0 then
28    let mode = "typeonly" in
29    let results =
30     let idx = ref ((page - 1) * results_per_page + List.length result + 1) in
31      List.fold_right
32       (fun uri i ->
33         decr idx ;
34         sprintf
35           "<tr>
36            <td valign=\"top\">%d.</td>
37            <td><span class=\"uri\">%s</span></td>
38            </tr>
39            <tr>
40            <td />
41            <td><ht:OBJECT uri=\"%s\" mode=\"%s\"/></td>
42            </tr>%s"
43           !idx uri uri mode i)
44       result ""
45    in
46    let summary =
47      sprintf "<b>%d</b> result%s found"
48        results_no (if results_no > 1 then "s" else "")
49    in
50    let results =
51      sprintf
52        "<table xmlns:ht=\"http://www.cs.unibo.it/helm/namespaces/helm-theory\">
53        %s
54        </table>"
55        results
56    in
57      (summary, results)
58   else
59     ("no results found", "")
60
61 let html_of_interpretations interps =
62   let choice_of_interp interp =
63     sprintf "<table>\n%s\n</table>"
64       (String.concat "\n"
65         (List.map
66            (fun (k, v) ->
67               sprintf "<tr><td><em>%s</em></td><td>%s</td></tr>" k v)
68            interp))
69   in
70   let interp_no = ref ~-1 in
71     sprintf "<table class=\"interp\">\n%s\n</table>"
72       (String.concat "\n"
73         (List.map
74            (fun interp ->
75               sprintf "
76                   <tr class=\"interp\">
77                   <td><input type=\"radio\" name=\"param.interp\" value=\"%d\" /></td>
78                   <td>
79                   %s
80                   </td></tr>"
81                 (incr interp_no; !interp_no)
82                 (choice_of_interp interp))
83            interps))
84