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