From: Claudio Sacerdoti Coen Date: Thu, 26 May 2005 16:04:05 +0000 (+0000) Subject: Now the links to 7 pages at a time are shown. Cool. X-Git-Tag: PRE_INDEX_1~117 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d747da7b7a32c08eb948f22ac505003a7adce2c4;p=helm.git Now the links to 7 pages at a time are shown. Cool. --- diff --git a/helm/searchEngine/html/moogle_trailer.html.src b/helm/searchEngine/html/moogle_trailer.html.src index 5f067c78a..be349ba52 100644 --- a/helm/searchEngine/html/moogle_trailer.html.src +++ b/helm/searchEngine/html/moogle_trailer.html.src @@ -4,6 +4,6 @@ xmlns="http://www.w3.org/1999/xhtml" >
- Page: @PREV_LINK@ @PAGE@/@PAGES@ @NEXT_LINK@ + @PAGES@: @PREV_LINK@ @PAGELIST@ @NEXT_LINK@
diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml index b7a699c2c..afb274f46 100644 --- a/helm/searchEngine/searchEngine.ml +++ b/helm/searchEngine/searchEngine.ml @@ -43,7 +43,7 @@ let placeholders = [ "ACTION"; "ADVANCED"; "ADVANCED_CHECKED"; "CHOICES"; "CURRENT_CHOICES"; "EXPRESSION"; "ID"; "IDEN"; "ID_TO_URIS"; "INTERPRETATIONS"; "INTERPRETATIONS_LABELS"; "MSG"; "NEW_ALIASES"; "NEXT_LINK"; "NO_CHOICES"; - "PAGE"; "PAGES"; "PREV_LINK"; "QUERY_KIND"; "QUERY_SUMMARY"; "RESULTS"; + "PAGE"; "PAGES"; "PAGELIST"; "PREV_LINK"; "QUERY_KIND"; "QUERY_SUMMARY"; "RESULTS"; "SEARCH_ENGINE_URL"; "SIMPLE_CHECKED"; "TITLE"; ] @@ -145,6 +145,14 @@ let patch_param param_name param_value url = (** HTML encoding, e.g.: "<" -> "<" *) let html_encode = Netencoding.Html.encode_from_latin1 +let fold_n_to_m f n m acc = + let rec aux acc = + function + i when i <= m -> aux (f i acc) (i + 1) + | _ -> acc + in + aux acc n + let send_results results ?(id_to_uris = CicTextualParser2.EnvironmentP3.of_string "") (req: Http_types.request) outchan @@ -181,9 +189,28 @@ let send_results results results_no / results_per_page + 1 in let pages = if pages = 0 then 1 else pages in + let additional_pages = 3 in let (summary, results) = MooglePp.theory_of_result page results in [ tag "PAGE", string_of_int page; - tag "PAGES", string_of_int pages; + tag "PAGES", string_of_int pages ^ " Pages"; + tag "PAGELIST", + (let inf = page - additional_pages in + let sup = page + additional_pages in + let superinf = inf - (sup - pages) in + let supersup = sup + (1 - inf) in + let n,m = + if inf >= 1 && sup <= pages then + inf,sup + else if inf < 1 then + 1, (if supersup <= pages then supersup else pages) + else (* sup > pages *) + (if superinf >= 1 then superinf else 1),pages + in + fold_n_to_m + (fun n acc -> acc ^ " " ^ + (if n = page then string_of_int n + else page_link (string_of_int n) n)) + n m ""); tag "PREV_LINK", (if page > 1 then page_link "Prev" (page-1) else ""); tag "NEXT_LINK", (if page < pages then page_link "Next" (page+1) else ""); @@ -192,7 +219,8 @@ let send_results results tag "RESULTS", results ] | `Error msg -> [ tag "PAGE", "1"; - tag "PAGES", "1"; + tag "PAGES", "1 Page"; + tag "PAGELIST", ""; tag "PREV_LINK", ""; tag "NEXT_LINK", ""; tag "QUERY_KIND", query_kind;