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   (** pretty print a list of URIs to an HELM theory file *)
  16 let theory_of_result req result =
  17   let max_results_no =
  18     Helm_registry.get_opt_default Helm_registry.get_int 10
  19       "search_engine.max_results_no"
  20   in
  21  let results_no = List.length result in
  22  let query_kind = pp_request req in
  23  let template query_kind summary results =
  24    sprintf
  25     "<div class='resultsbar'>
  26       <table width='100%%'>
  27        <tr>
  28         <td class='left'><b class='query_kind'>%s</b></td>
  29         <td class='right'>%s</td>
  30        </tr>
  31       </table>
  32      </div>
  33      <br />
  34      <div>
  35      %s
  36      </div>"
  37      query_kind summary results
  38  in
  39   if results_no > 0 then
  40    let mode = if results_no > max_results_no then "linkonly" else "typeonly" in
  41    let results =
  42     let idx = ref (results_no + 1) in
  43      List.fold_right
  44       (fun uri i ->
  45         decr idx ;
  46         sprintf
  47           "<tr>
  48            <td valign=\"top\">%d.</td>
  49            <td><ht:OBJECT uri=\"%s\" mode=\"%s\"/></td>
  50            </tr>%s"
  51           !idx uri mode i)
  52       result ""
  53    in
  54    template query_kind
  55     (sprintf "<b>%d</b> result%s found"
  56       results_no (if results_no > 1 then "s" else ""))
  57     (sprintf
  58       "<table xmlns:ht=\"http://www.cs.unibo.it/helm/namespaces/helm-theory\">
  59         %s
  60        </table>"
  61        results)
  62   else
  63     template query_kind "no results found" ""
  64
  65 let html_of_interpretations interps =
  66   let radio_button n =
  67     sprintf "<input type=\"radio\" name=\"param.interp\" value=\"%d\" />" n
  68   in
  69   let text interp =
  70     String.concat "<br />"
  71       (List.map
  72          (fun (id, value) -> sprintf "<span>%s = %s</span>" id value)
  73          interp)
  74   in
  75   let rec aux n = function
  76     | [] -> []
  77     | interp::tl -> ((radio_button n)^(text interp))::(aux (n+1) tl)
  78   in
  79   String.concat "<br />" (aux 0 interps)
  80