- reimplemented basic features using the helm-metadata library instead

[helm.git] / helm / searchEngine / mooglePp.ml

diff --git a/helm/searchEngine/mooglePp.ml b/helm/searchEngine/mooglePp.ml
new file mode 100644 (file)
index 0000000..807fcc2
--- /dev/null
+++ b/helm/searchEngine/mooglePp.ml
@@ -0,0 +1,80 @@
+
+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)
+