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 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: 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 %s

%s
" query_kind summary results in if results_no > 0 then let mode = "typeonly" in let results = 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 uri mode i) result "" in template query_kind (sprintf "%d result%s found" results_no (if results_no > 1 then "s" else "")) (sprintf " %s
" results) else template query_kind "no results found" "" let html_of_interpretations interps = let radio_button n = sprintf "" n in let text interp = String.concat "
" (List.map (fun (id, value) -> sprintf "%s = %s" id value) interp) in let rec aux n = function | [] -> [] | interp::tl -> ((radio_button n)^(text interp))::(aux (n+1) tl) in String.concat "
" (aux 0 interps)