]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/searchEngine/mooglePp.ml
daemons tamed
[helm.git] / helm / searchEngine / mooglePp.ml
diff --git a/helm/searchEngine/mooglePp.ml b/helm/searchEngine/mooglePp.ml
deleted file mode 100644 (file)
index 3af0afb..0000000
+++ /dev/null
@@ -1,83 +0,0 @@
-
-open Printf
-
-let pp_error 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 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
-  if results_no > 0 then
-   let mode = "typeonly" in
-   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
-    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
-    ("no results found", "")
-
-let html_of_interpretations interps =
-  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
-  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))
-