" 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 page result =
let results_per_page =
Helm_registry.get_int "search_engine.results_per_page"
in
let results_no = List.length result in
let buffer = Buffer.create (200 * results_no) in
let result = paginate ~size:results_per_page ~page result in
if results_no > 0 then
let mode = "typeonly" in
let output_results () =
let idx = ref ((page - 1) * results_per_page) in
List.iter
(fun uri ->
incr idx;
Printf.bprintf buffer
"
%d.
%s
"
!idx uri uri mode) result ;
in
let summary =
sprintf "%d result%s found"
results_no (if results_no > 1 then "s" else "")
in
begin
Buffer.add_string buffer
"
";
output_results ();
Buffer.add_string buffer "
";
(summary, Buffer.contents buffer)
end
else
("no results found", "")
let html_of_interpretations interps =
let choice_of_interp interp =
sprintf "