X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2FsearchEngine%2FmooglePp.ml;h=50809a45940bc9f05383d2c70c9298df8e9aea00;hb=f38e8fafcf040258b54b4032562753a876a8a94e;hp=807fcc219180dc68989c88a6082b4d9c486a74c0;hpb=ffb569818f6e4d9723dbd2c1721bbe80e75278e9;p=helm.git
diff --git a/helm/searchEngine/mooglePp.ml b/helm/searchEngine/mooglePp.ml
index 807fcc219..50809a459 100644
--- a/helm/searchEngine/mooglePp.ml
+++ b/helm/searchEngine/mooglePp.ml
@@ -12,43 +12,62 @@ let pp_request (req: Http_types.request) =
let pp_error title msg =
sprintf "
%s: %s
" 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
+ "
+
+
+
+ %s
+
+ "
+ 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
- "
-
-
- %s
-
"
- 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 ;
sprintf
"
%d. |
+ %s |
+
+
+ |
|
%s"
- !idx uri mode i)
+ !idx uri uri mode i)
result ""
in
template query_kind