- re-enginered main moogle template, it is now aware of queries kind, summary,

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

diff --git a/helm/searchEngine/mooglePp.ml b/helm/searchEngine/mooglePp.ml
index 50809a45940bc9f05383d2c70c9298df8e9aea00..7731eb28802998de47f3e10ae6ce0c9133664eec 100644 (file)
--- a/helm/searchEngine/mooglePp.ml
+++ b/helm/searchEngine/mooglePp.ml
@@ -1,16 +1,8 @@
 
 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
+  sprintf "<div><b class='error'>%s:</b> %s</div><br />" title msg
 
 let paginate ~size ~page l =
   let min = 1 + (page-1) * size in
@@ -26,31 +18,12 @@ let paginate ~size ~page l =
   aux 1 l
 
   (** pretty print a list of URIs to an HELM theory file *)
-let theory_of_result (req: Http_types.request) page result =
+let theory_of_result page result =
   let results_per_page =
     Helm_registry.get_int "search_engine.results_per_page"
   in
   let results_no = List.length result in
   let result = paginate ~size:results_per_page ~page result in
-  let query_kind = pp_request req in
-  let template query_kind summary results =
-    sprintf
-      "<!-- MOZILLA SEARCH PLUGIN: BEGIN LIST -->
-       <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>
-       <!-- MOZILLA SEARCH PLUGIN: END LIST -->"
-       query_kind summary results
-  in
   if results_no > 0 then
    let mode = "typeonly" in
    let results =
@@ -70,16 +43,20 @@ let theory_of_result (req: Http_types.request) page result =
           !idx uri 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
+   let summary =
+     sprintf "<b>%d</b> result%s found"
+       results_no (if results_no > 1 then "s" else "")
+   in
+   let results =
+     sprintf
+       "<table xmlns:ht=\"http://www.cs.unibo.it/helm/namespaces/helm-theory\">
+       %s
        </table>"
-       results)
+       results
+   in
+     (summary, results)
   else
-    template query_kind "no results found" ""
+    ("no results found", "")
 
 let html_of_interpretations interps =
   let radio_button n =