From: Stefano Zacchiroli Date: Wed, 16 Mar 2005 10:23:37 +0000 (+0000) Subject: - re-enginered main moogle template, it is now aware of queries kind, summary, X-Git-Tag: old_htmls~3 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2a36d2bb28a102199c2dbd9cef762bccab3c7824;p=helm.git - re-enginered main moogle template, it is now aware of queries kind, summary, and results. This enable fixing of minor like feedback on the query kind in case of errors - minor bug fixes: 1/0 nuisance in case of errors - commented out advanced query selection (which do nothing) --- diff --git a/helm/searchEngine/html/moogle.html b/helm/searchEngine/html/moogle.html index a128cef49..f1ace2df4 100644 --- a/helm/searchEngine/html/moogle.html +++ b/helm/searchEngine/html/moogle.html @@ -51,11 +51,10 @@ +
+ + +
+ + + + + +
@QUERY_KIND@@QUERY_SUMMARY@
+
+
+
@RESULTS@ +
+
diff --git a/helm/searchEngine/mooglePp.ml b/helm/searchEngine/mooglePp.ml index 50809a459..7731eb288 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%s
-
-
-
- %s -
- " - query_kind summary results - in if results_no > 0 then let mode = "typeonly" in let results = @@ -70,16 +43,20 @@ 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 - " - %s + let summary = + sprintf "%d result%s found" + results_no (if results_no > 1 then "s" else "") + in + let results = + sprintf + "
+ %s
" - results) + results + in + (summary, results) else - template query_kind "no results found" "" + ("no results found", "") let html_of_interpretations interps = let radio_button n = diff --git a/helm/searchEngine/mooglePp.mli b/helm/searchEngine/mooglePp.mli index 18a169d0b..f3e2e5952 100644 --- a/helm/searchEngine/mooglePp.mli +++ b/helm/searchEngine/mooglePp.mli @@ -1,3 +1,35 @@ +(* Copyright (C) 2002-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + val pp_error : string -> string -> string -val theory_of_result : Http_types.request -> int -> string list -> string + +(** @param page page number + * @param results query results + * @return a pair of suitable instantiations for + * QUERY_SUMMARY and QUERY_RESULTS tag in moogle's main template *) +val theory_of_result : int -> string list -> string * string + val html_of_interpretations: (string * string) list list -> string + diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml index 87546b1ff..9fa4caa26 100644 --- a/helm/searchEngine/searchEngine.ml +++ b/helm/searchEngine/searchEngine.ml @@ -1,4 +1,4 @@ -(* Copyright (C) 2002-2004, HELM Team. +(* Copyright (C) 2002-2005, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -34,14 +34,15 @@ exception Unbound_identifier of string exception Invalid_action of string (* invalid action for "/search" method *) let daemon_name = "Moogle" -let configuration_file = "/projects/helm/etc/moogle.conf.xml" -(*let configuration_file = "searchEngine.conf.xml" *) +let configuration_file = + "/projects/helm/daemons/searchEngine.debug/moogle.conf.xml" let placeholders = [ - "EXPRESSION"; "ACTION"; "ADVANCED"; "ADVANCED_CHECKED"; "SIMPLE_CHECKED"; - "TITLE"; "NO_CHOICES"; "CURRENT_CHOICES"; "CHOICES"; "MSG"; "ID_TO_URIS"; - "ID"; "IDEN"; "INTERPRETATIONS"; "INTERPRETATIONS_LABELS"; "RESULTS"; - "NEW_ALIASES"; "SEARCH_ENGINE_URL"; "PREV_LINK"; "PAGE"; "PAGES"; "NEXT_LINK" + "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"; + "SEARCH_ENGINE_URL"; "SIMPLE_CHECKED"; "TITLE"; ] let tag = @@ -49,7 +50,10 @@ let tag = List.iter (fun tag -> Hashtbl.add regexps tag (Pcre.regexp (sprintf "@%s@" tag))) placeholders; - Hashtbl.find regexps + fun name -> + try + Hashtbl.find regexps name + with Not_found -> assert false (* First of all we load the configuration *) let _ = Helm_registry.load_from configuration_file @@ -113,10 +117,19 @@ let add_param_substs params = let page_RE = Pcre.regexp "¶m\\.page=\\d+" +let query_kind_of_req (req: Http_types.request) = + match req#path with + | "/match" -> "Match" + | "/hint" -> "Hint" + | "/locate" -> "Locate" + | "/elim" -> "Elim" + | _ -> assert false + let send_results results ?(id_to_uris = CicTextualParser2.EnvironmentP3.of_string "") (req: Http_types.request) outchan = + let query_kind = query_kind_of_req req in let page_link anchor page = try let this = req#param "this" in @@ -134,7 +147,7 @@ let send_results results Http_daemon.send_basic_headers ~code:(`Code 200) outchan ; Http_daemon.send_header "Content-Type" "text/xml" outchan; Http_daemon.send_CRLF outchan ; - let subst, results_string = + let subst = match results with | `Results results -> let page = try int_of_string (req#param "page") with _ -> 1 in @@ -148,24 +161,36 @@ let send_results results else results_no / results_per_page + 1 in - ([ tag "PAGE", string_of_int page; tag "PAGES", string_of_int pages ] @ - [ 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 "" ]), - MooglePp.theory_of_result req page results + let pages = if pages = 0 then 1 else pages in + let (summary, results) = MooglePp.theory_of_result page results in + [ tag "PAGE", string_of_int page; + tag "PAGES", string_of_int pages; + 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 ""); + tag "QUERY_KIND", query_kind; + tag "QUERY_SUMMARY", summary; + tag "RESULTS", results ] | `Error msg -> - [ tag "PAGE", ""; tag "PAGES", ""; - tag "PREV_LINK", ""; tag "NEXT_LINK", "" ], - msg + [ tag "PAGE", "1"; + tag "PAGES", "1"; + tag "PREV_LINK", ""; + tag "NEXT_LINK", ""; + tag "QUERY_KIND", query_kind; + tag "QUERY_SUMMARY", "error"; + tag "RESULTS", msg ] + in + let advanced = + try + req#param "advanced" + with Http_types.Param_not_found _ -> "no" in let subst = (tag "SEARCH_ENGINE_URL", my_own_url) :: - (tag "RESULTS", results_string) :: - (tag "ADVANCED", req#param "advanced") :: + (tag "ADVANCED", advanced) :: (tag "EXPRESSION", req#param "expression") :: add_param_substs req#params @ - (if req#param "advanced" = "no" then + (if advanced = "no" then [ tag "SIMPLE_CHECKED", "checked='true'"; tag "ADVANCED_CHECKED", "" ] else @@ -245,11 +270,16 @@ let exec_action dbd (req: Http_types.request) outchan = in Http_daemon.send_basic_headers ~code:(`Code 200) outchan ; Http_daemon.send_CRLF outchan ; + let advanced = + try + req#param "advanced" + with Http_types.Param_not_found _ -> "no" + in iter_file (fun line -> let processed_line = apply_substs - [tag "ADVANCED", req#param "advanced"; + [tag "ADVANCED", advanced; tag "INTERPRETATIONS", html_interpretations; tag "CURRENT_CHOICES", req#param "choices"; tag "EXPRESSION", req#param "expression"; @@ -344,9 +374,10 @@ let callback dbd (req: Http_types.request) outchan = in if expression = "" then send_results (`Results []) req outchan - else + else begin let results = MetadataQuery.locate ~dbd expression in send_results (`Results results) req outchan + end | "/hint" | "/elim" | "/match" -> exec_action dbd req outchan