X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FsearchEngine%2FmooglePp.ml;h=3af0afb4051f882f5251d44891ecc787c93cc232;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=998274e08525e60bd7d38a297d210ea1ae419d87;hpb=5cb2fa1e3e6f5d9d7a273b45c56a6c1196982c4a;p=helm.git

diff --git a/helm/searchEngine/mooglePp.ml b/helm/searchEngine/mooglePp.ml
index 998274e08..3af0afb40 100644
--- 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,68 +18,66 @@ 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 buffer = Buffer.create (200 * results_no) 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
-      "<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 = "typeonly" in
-   let results =
-    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><ht:OBJECT uri=\"%s\" mode=\"%s\"/></td>
-           </tr>%s"
-          !idx uri mode i)
-      result ""
+   let output_results () =
+    let idx = ref ((page - 1) * results_per_page) in
+     List.iter
+      (fun uri ->
+        incr idx;
+        Printf.bprintf buffer 
+           "<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>"
+          !idx uri uri mode) result ;
+   in
+   let summary =
+     sprintf "<b>%d</b> result%s found"
+       results_no (if results_no > 1 then "s" else "")
    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)
+    begin
+     Buffer.add_string buffer
+      "<table xmlns:ht=\"http://www.cs.unibo.it/helm/namespaces/helm-theory\">";
+     output_results ();
+     Buffer.add_string buffer "</table>";
+     (summary, Buffer.contents buffer)
+    end
   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))