X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2FsearchEngine%2FmooglePp.ml;h=92b55668e5cbe9aa1f5e69194df01c8887d7b37b;hb=8e8dcd3aa99386578b4002a09696884f61941306;hp=807fcc219180dc68989c88a6082b4d9c486a74c0;hpb=ffb569818f6e4d9723dbd2c1721bbe80e75278e9;p=helm.git
diff --git a/helm/searchEngine/mooglePp.ml b/helm/searchEngine/mooglePp.ml
index 807fcc219..92b55668e 100644
--- a/helm/searchEngine/mooglePp.ml
+++ b/helm/searchEngine/mooglePp.ml
@@ -1,80 +1,84 @@
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 "
%s: %s
" 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 page result =
+ let results_per_page =
+ Helm_registry.get_int "search_engine.results_per_page"
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
+ let results_no = List.length result in
+ let result = paginate ~size:results_per_page ~page result 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
- (sprintf "%d result%s found"
- results_no (if results_no > 1 then "s" else ""))
- (sprintf
- "