helm/searchEngine/mooglePp.ml

   1
   2 open Printf
   3
   4 let pp_request (req: Http_types.request) =
   5   match req#path with
   6   | "/elim" -> "Elim"
   7   | "/match" -> "Match"
   8   | "/hint" -> "Hint"
   9   | "/locate" -> "Locate"
  10   | _ -> assert false
  11
  12 let pp_error title msg =
  13   sprintf "<hr size='1' /><div><b class='error'>%s:</b> %s</div>" title msg
  14
  15 let paginate ~size ~page l =
  16   let min = 1 + (page-1) * size in
  17   let max = page * size in
  18   let rec aux i l =
  19     match (i, l) with
  20     | _, [] -> []
  21     | i, hd :: tl when i < min -> aux (i+1) tl
  22     | i, hd :: tl when i >= min && i <= max -> hd :: aux (i+1) tl
  23     | i, hd :: tl -> []
  24   in
  25   assert (size > 0 && page > 0);
  26   aux 1 l
  27
  28   (** pretty print a list of URIs to an HELM theory file *)
  29 let theory_of_result (req: Http_types.request) page result =
  30   let results_per_page =
  31     Helm_registry.get_int "search_engine.results_per_page"
  32   in
  33   let results_no = List.length result in
  34   let result = paginate ~size:results_per_page ~page result in
  35   let query_kind = pp_request req in
  36   let template query_kind summary results =
  37     sprintf
  38       "<!-- MOZILLA SEARCH PLUGIN: BEGIN LIST -->
  39        <div class='resultsbar'>
  40         <table width='100%%'>
  41          <tr>
  42           <td class='left'><b class='query_kind'>%s</b></td>
  43           <td class='right'>%s</td>
  44          </tr>
  45         </table>
  46        </div>
  47        <br />
  48        <div>
  49        %s
  50        </div>
  51        <!-- MOZILLA SEARCH PLUGIN: END LIST -->"
  52        query_kind summary results
  53   in
  54   if results_no > 0 then
  55    let mode = "typeonly" in
  56    let results =
  57     let idx = ref ((page - 1) * results_per_page + List.length result + 1) in
  58      List.fold_right
  59       (fun uri i ->
  60         decr idx ;
  61         sprintf
  62           "<tr>
  63            <td valign=\"top\">%d.</td>
  64            <td><span class=\"uri\">%s</span></td>
  65            </tr>
  66            <tr>
  67            <td />
  68            <td><ht:OBJECT uri=\"%s\" mode=\"%s\"/></td>
  69            </tr>%s"
  70           !idx uri uri mode i)
  71       result ""
  72    in
  73    template query_kind
  74     (sprintf "<b>%d</b> result%s found"
  75       results_no (if results_no > 1 then "s" else ""))
  76     (sprintf
  77       "<table xmlns:ht=\"http://www.cs.unibo.it/helm/namespaces/helm-theory\">
  78         %s
  79        </table>"
  80        results)
  81   else
  82     template query_kind "no results found" ""
  83
  84 let html_of_interpretations interps =
  85   let radio_button n =
  86     sprintf "<input type=\"radio\" name=\"param.interp\" value=\"%d\" />" n
  87   in
  88   let text interp =
  89     String.concat "<br />"
  90       (List.map
  91          (fun (id, value) -> sprintf "<span>%s = %s</span>" id value)
  92          interp)
  93   in
  94   let rec aux n = function
  95     | [] -> []
  96     | interp::tl -> ((radio_button n)^(text interp))::(aux (n+1) tl)
  97   in
  98   String.concat "<br />" (aux 0 interps)
  99