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"
!idx 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)