helm/searchEngine/mooglePp.ml

   1
   2 open Printf
   3
   4 let pp_error title msg =
   5   sprintf "<div><b class='error'>%s:</b> %s</div><br />" title msg
   6
   7 let paginate ~size ~page l =
   8   let min = 1 + (page-1) * size in
   9   let max = page * size in
  10   let rec aux i l =
  11     match (i, l) with
  12     | _, [] -> []
  13     | i, hd :: tl when i < min -> aux (i+1) tl
  14     | i, hd :: tl when i >= min && i <= max -> hd :: aux (i+1) tl
  15     | i, hd :: tl -> []
  16   in
  17   assert (size > 0 && page > 0);
  18   aux 1 l
  19
  20   (** pretty print a list of URIs to an HELM theory file *)
  21 let theory_of_result page result =
  22   let results_per_page =
  23     Helm_registry.get_int "search_engine.results_per_page"
  24   in
  25   let results_no = List.length result in
  26   let result = paginate ~size:results_per_page ~page result in
  27   if results_no > 0 then
  28    let mode = "typeonly" in
  29    let results =
  30     let idx = ref ((page - 1) * results_per_page + List.length result + 1) in
  31      List.fold_right
  32       (fun uri i ->
  33         decr idx ;
  34         sprintf
  35           "<tr>
  36            <td valign=\"top\">%d.</td>
  37            <td><span class=\"uri\">%s</span></td>
  38            </tr>
  39            <tr>
  40            <td />
  41            <td><ht:OBJECT uri=\"%s\" mode=\"%s\"/></td>
  42            </tr>%s"
  43           !idx uri uri mode i)
  44       result ""
  45    in
  46    let summary =
  47      sprintf "<b>%d</b> result%s found"
  48        results_no (if results_no > 1 then "s" else "")
  49    in
  50    let results =
  51      sprintf
  52        "<table xmlns:ht=\"http://www.cs.unibo.it/helm/namespaces/helm-theory\">
  53        %s
  54        </table>"
  55        results
  56    in
  57      (summary, results)
  58   else
  59     ("no results found", "")
  60
  61 let html_of_interpretations interps =
  62   let radio_button n =
  63     sprintf "<input type=\"radio\" name=\"param.interp\" value=\"%d\" />" n
  64   in
  65   let text interp =
  66     String.concat "<br />"
  67       (List.map
  68          (fun (id, value) -> sprintf "<span>%s = %s</span>" id value)
  69          interp)
  70   in
  71   let rec aux n = function
  72     | [] -> []
  73     | interp::tl -> ((radio_button n)^(text interp))::(aux (n+1) tl)
  74   in
  75   String.concat "<br />" (aux 0 interps)
  76