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 "<hr size='1' /><div><b class='error'>%s:</b> %s</div>" title msg

  (** pretty print a list of URIs to an HELM theory file *)
let theory_of_result req result =
  let max_results_no =
    Helm_registry.get_opt_default Helm_registry.get_int 10
      "search_engine.max_results_no"
  in
 let results_no = List.length result in
 let query_kind = pp_request req in
 let template query_kind summary results =
   sprintf
    "<div class='resultsbar'>
      <table width='100%%'>
       <tr>
        <td class='left'><b class='query_kind'>%s</b></td>
        <td class='right'>%s</td>
       </tr>
      </table>
     </div>
     <br />
     <div>
     %s
     </div>"
     query_kind summary results
 in
  if results_no > 0 then
   let mode = if results_no > max_results_no then "linkonly" else "typeonly" in
   let results =
    let idx = ref (results_no + 1) in
     List.fold_right
      (fun uri i ->
        decr idx ;
        sprintf
          "<tr>
           <td valign=\"top\">%d.</td>
           <td><ht:OBJECT uri=\"%s\" mode=\"%s\"/></td>
           </tr>%s"
          !idx uri mode i)
      result ""
   in
   template query_kind
    (sprintf "<b>%d</b> result%s found"
      results_no (if results_no > 1 then "s" else ""))
    (sprintf
      "<table xmlns:ht=\"http://www.cs.unibo.it/helm/namespaces/helm-theory\">
        %s
       </table>"
       results)
  else
    template query_kind "no results found" ""

let html_of_interpretations interps =
  let radio_button n = 
    sprintf "<input type=\"radio\" name=\"param.interp\" value=\"%d\" />" n
  in
  let text interp =
    String.concat "<br />" 
      (List.map
         (fun (id, value) -> sprintf "<span>%s = %s</span>" id value)
         interp)
  in
  let rec aux n = function
    | [] -> []
    | interp::tl -> ((radio_button n)^(text interp))::(aux (n+1) tl)
  in
  String.concat "<br />" (aux 0 interps)