X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2FsearchEngine%2FmooglePp.ml;h=92b55668e5cbe9aa1f5e69194df01c8887d7b37b;hb=aca103d3c3d740efcc0bcc2932922cff77facb49;hp=50809a45940bc9f05383d2c70c9298df8e9aea00;hpb=3f6f868f14eadef7f17d5e3008cffe19307ad492;p=helm.git
diff --git a/helm/searchEngine/mooglePp.ml b/helm/searchEngine/mooglePp.ml
index 50809a459..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,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
- "
-
-
-
- %s
-
- "
- query_kind summary results
- in
if results_no > 0 then
let mode = "typeonly" in
let results =
@@ -70,30 +43,42 @@ let theory_of_result (req: Http_types.request) page result =
!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
- "