X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FsearchEngine%2FmooglePp.ml;h=998274e08525e60bd7d38a297d210ea1ae419d87;hb=ac7687ce66526f905874ed99a845223c853c558a;hp=807fcc219180dc68989c88a6082b4d9c486a74c0;hpb=ffb569818f6e4d9723dbd2c1721bbe80e75278e9;p=helm.git

diff --git a/helm/searchEngine/mooglePp.ml b/helm/searchEngine/mooglePp.ml
index 807fcc219..998274e08 100644
--- a/helm/searchEngine/mooglePp.ml
+++ b/helm/searchEngine/mooglePp.ml
@@ -12,34 +12,47 @@ let pp_request (req: Http_types.request) =
 let pp_error title msg =
   sprintf "<hr size='1' /><div><b class='error'>%s:</b> %s</div>" title msg
 
+let paginate ~size ~page l =
+  let min = 1 + (page-1) * size in
+  let max = page * size in
+  let rec aux i l =
+    match (i, l) with
+    | _, [] -> []
+    | i, hd :: tl when i < min -> aux (i+1) tl
+    | i, hd :: tl when i >= min && i <= max -> hd :: aux (i+1) tl
+    | i, hd :: tl -> []
+  in
+  assert (size > 0 && page > 0);
+  aux 1 l
+
   (** pretty print a list of URIs to an HELM theory file *)
-let theory_of_result req result =
-  let max_results_no =
-    Helm_registry.get_opt_default Helm_registry.get_int 10
-      "search_engine.max_results_no"
+let theory_of_result (req: Http_types.request) page result =
+  let results_per_page =
+    Helm_registry.get_int "search_engine.results_per_page"
+  in
+  let results_no = List.length result 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
+      "<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>"
+       query_kind summary results
   in
- let results_no = List.length result in
- let query_kind = pp_request req in
- let template query_kind summary results =
-   sprintf
-    "<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>"
-     query_kind summary results
- in
   if results_no > 0 then
-   let mode = if results_no > max_results_no then "linkonly" else "typeonly" in
+   let mode = "typeonly" in
    let results =
-    let idx = ref (results_no + 1) in
+    let idx = ref ((page - 1) * results_per_page + List.length result + 1) in
      List.fold_right
       (fun uri i ->
         decr idx ;