X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FsearchEngine%2FmooglePp.ml;h=92b55668e5cbe9aa1f5e69194df01c8887d7b37b;hb=6912a028bef118d8e9d7c2847200510a9b055c6a;hp=807fcc219180dc68989c88a6082b4d9c486a74c0;hpb=ffb569818f6e4d9723dbd2c1721bbe80e75278e9;p=helm.git

diff --git a/helm/searchEngine/mooglePp.ml b/helm/searchEngine/mooglePp.ml
index 807fcc219..92b55668e 100644
--- a/helm/searchEngine/mooglePp.ml
+++ b/helm/searchEngine/mooglePp.ml
@@ -1,80 +1,84 @@
 
 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
+  let max = page * size in
+  let rec aux i l =
+    match (i, l) with
+    | _, [] -> []
+    | i, hd :: tl when i < min -> aux (i+1) tl
+    | i, hd :: tl when i >= min && i <= max -> hd :: aux (i+1) tl
+    | i, hd :: tl -> []
+  in
+  assert (size > 0 && page > 0);
+  aux 1 l
 
   (** 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"
+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 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
+  let results_no = List.length result in
+  let result = paginate ~size:results_per_page ~page result in
   if results_no > 0 then
-   let mode = if results_no > max_results_no then "linkonly" else "typeonly" in
+   let mode = "typeonly" in
    let results =
-    let idx = ref (results_no + 1) in
+    let idx = ref ((page - 1) * results_per_page + List.length result + 1) in
      List.fold_right
       (fun uri i ->
         decr idx ;
         sprintf
           "<tr>
            <td valign=\"top\">%d.</td>
+           <td><span class=\"uri\">%s</span></td>
+           </tr>
+           <tr>
+           <td />
            <td><ht:OBJECT uri=\"%s\" mode=\"%s\"/></td>
            </tr>%s"
-          !idx uri mode i)
+          !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 = 
-    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)
+  let choice_of_interp interp =
+    sprintf "<table>\n%s\n</table>"
+      (String.concat "\n"
+        (List.map
+           (fun (k, v) ->
+              sprintf "<tr><td><em>%s</em></td><td>%s</td></tr>" k v)
+           interp))
   in
-  String.concat "<br />" (aux 0 interps)
+  let interp_no = ref ~-1 in
+    sprintf "<table class=\"interp\">\n%s\n</table>"
+      (String.concat "\n"
+        (List.map
+           (fun interp ->
+              sprintf "
+                  <tr class=\"interp\">
+                  <td><input type=\"radio\" name=\"param.interp\" value=\"%d\" /></td>
+                  <td>
+                  %s
+                  </td></tr>"
+                (incr interp_no; !interp_no)
+                (choice_of_interp interp))
+           interps))