X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2FsearchEngine%2FmooglePp.ml;h=92b55668e5cbe9aa1f5e69194df01c8887d7b37b;hb=31afc64440b7da53bb79e6f1524d47bf0fb56aaf;hp=998274e08525e60bd7d38a297d210ea1ae419d87;hpb=5cb2fa1e3e6f5d9d7a273b45c56a6c1196982c4a;p=helm.git
diff --git a/helm/searchEngine/mooglePp.ml b/helm/searchEngine/mooglePp.ml
index 998274e08..92b55668e 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 "
%s: %s
" title msg
+ sprintf "%s: %s
" title msg
let paginate ~size ~page l =
let min = 1 + (page-1) * size in
@@ -26,29 +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
- "
-
-
- %s
-
"
- query_kind summary results
- in
if results_no > 0 then
let mode = "typeonly" in
let results =
@@ -59,35 +34,51 @@ let theory_of_result (req: Http_types.request) page result =
sprintf
"
%d. |
+ %s |
+
+
+ |
|
%s"
- !idx uri mode i)
+ !idx uri uri mode i)
result ""
in
- template query_kind
- (sprintf "%d result%s found"
- results_no (if results_no > 1 then "s" else ""))
- (sprintf
- "