]> matita.cs.unibo.it Git - helm.git/commitdiff
- re-enginered main moogle template, it is now aware of queries kind, summary,
authorStefano Zacchiroli <zack@upsilon.cc>
Wed, 16 Mar 2005 10:23:37 +0000 (10:23 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Wed, 16 Mar 2005 10:23:37 +0000 (10:23 +0000)
  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)

helm/searchEngine/html/moogle.html
helm/searchEngine/mooglePp.ml
helm/searchEngine/mooglePp.mli
helm/searchEngine/searchEngine.ml

index a128cef492ecd1d48c8216de2d22847e7e6a4cd2..f1ace2df4f38cd1ec5c7b362ee59bea8059578ca 100644 (file)
    </font>
   </td>
   </tr>
+  <br />
+<!--
   <tr>
-  </tr>
-  <tr>
-   <td> </td>
-   <td> </td>
+   <td colspan="2" />
    <td align="center">
     <font size="-1">
     <input type="radio" name="param.advanced" value="no" @SIMPLE_CHECKED@ />
     <label>Advanced search</label>
     </font>
    </td>
-   <td> </td>
-   <td> </td>
+   <td colspan="2" />
    </tr>
+-->
   </table>
 </helm:uwobo_form>
 <font size="-1">
+<!-- MOZILLA SEARCH PLUGIN: BEGIN LIST -->
+ <div class='resultsbar'>
+  <table width='100%%'>
+   <tr>
+    <td class='left'><b class='query_kind'>@QUERY_KIND@</b></td>
+    <td class='right'>@QUERY_SUMMARY@</td>
+   </tr>
+  </table>
+ </div>
+ <br />
+ <div>
 @RESULTS@
+ </div>
+ <!-- MOZILLA SEARCH PLUGIN: END LIST -->
 </font>
 <font size="-1">
   <div class='bottombar'>
index 50809a45940bc9f05383d2c70c9298df8e9aea00..7731eb28802998de47f3e10ae6ce0c9133664eec 100644 (file)
@@ -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 "<hr size='1' /><div><b class='error'>%s:</b> %s</div>" 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
@@ -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
-      "<!-- MOZILLA SEARCH PLUGIN: BEGIN LIST -->
-       <div class='resultsbar'>
-        <table width='100%%'>
-         <tr>
-          <td class='left'><b class='query_kind'>%s</b></td>
-          <td class='right'>%s</td>
-         </tr>
-        </table>
-       </div>
-       <br />
-       <div>
-       %s
-       </div>
-       <!-- MOZILLA SEARCH PLUGIN: END LIST -->"
-       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 "<b>%d</b> result%s found"
-      results_no (if results_no > 1 then "s" else ""))
-    (sprintf
-      "<table xmlns:ht=\"http://www.cs.unibo.it/helm/namespaces/helm-theory\">
-        %s
+   let summary =
+     sprintf "<b>%d</b> result%s found"
+       results_no (if results_no > 1 then "s" else "")
+   in
+   let results =
+     sprintf
+       "<table xmlns:ht=\"http://www.cs.unibo.it/helm/namespaces/helm-theory\">
+       %s
        </table>"
-       results)
+       results
+   in
+     (summary, results)
   else
-    template query_kind "no results found" ""
+    ("no results found", "")
 
 let html_of_interpretations interps =
   let radio_button n = 
index 18a169d0b19cfead7992fec94d2e790596cd49ad..f3e2e595226e4c8ec7b7cbab3efc55a5c3413464 100644 (file)
@@ -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 <summary, results> 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
+
index 87546b1ffdff61fbdd0a73e93a859aa087427674..9fa4caa26f8b2f96d7f408c38b0a17ec21ec6ef8 100644 (file)
@@ -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 "&param\\.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