From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 16 Mar 2005 16:17:03 +0000 (+0000)
Subject: - new pretty printing of interpretations
X-Git-Tag: V_0_6_3_3~5
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a240236d1e9d5154e8cb5da73f8e98cf7734a73e;p=helm.git

- new pretty printing of interpretations
- bugfix: interpretations are now remembered between pages
- more coherent look and feel
---

diff --git a/helm/searchEngine/mooglePp.ml b/helm/searchEngine/mooglePp.ml
index 7731eb288..92b55668e 100644
--- a/helm/searchEngine/mooglePp.ml
+++ b/helm/searchEngine/mooglePp.ml
@@ -59,18 +59,26 @@ let theory_of_result page result =
     ("no results found", "")
 
 let html_of_interpretations interps =
-  let radio_button n = 
-    sprintf "<input type=\"radio\" name=\"param.interp\" value=\"%d\" />" n
+  let choice_of_interp interp =
+    sprintf "<table>\n%s\n</table>"
+      (String.concat "\n"
+        (List.map
+           (fun (k, v) ->
+              sprintf "<tr><td><em>%s</em></td><td>%s</td></tr>" k v)
+           interp))
   in
-  let text interp =
-    String.concat "<br />" 
-      (List.map
-         (fun (id, value) -> sprintf "<span>%s = %s</span>" id value)
-         interp)
-  in
-  let rec aux n = function
-    | [] -> []
-    | interp::tl -> ((radio_button n)^(text interp))::(aux (n+1) tl)
-  in
-  String.concat "<br />" (aux 0 interps)
+  let interp_no = ref ~-1 in
+    sprintf "<table class=\"interp\">\n%s\n</table>"
+      (String.concat "\n"
+        (List.map
+           (fun interp ->
+              sprintf "
+                  <tr class=\"interp\">
+                  <td><input type=\"radio\" name=\"param.interp\" value=\"%d\" /></td>
+                  <td>
+                  %s
+                  </td></tr>"
+                (incr interp_no; !interp_no)
+                (choice_of_interp interp))
+           interps))
 
diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml
index 9fa4caa26..d994ac11a 100644
--- a/helm/searchEngine/searchEngine.ml
+++ b/helm/searchEngine/searchEngine.ml
@@ -34,8 +34,7 @@ exception Unbound_identifier of string
 exception Invalid_action of string  (* invalid action for "/search" method *)
 
 let daemon_name = "Moogle"
-let configuration_file =
-  "/projects/helm/daemons/searchEngine.debug/moogle.conf.xml"
+let configuration_file = "/projects/helm/etc/moogle.conf.xml"
 
 let placeholders = [
   "ACTION"; "ADVANCED"; "ADVANCED_CHECKED"; "CHOICES"; "CURRENT_CHOICES";
@@ -60,8 +59,8 @@ let _ = Helm_registry.load_from configuration_file
 let port = Helm_registry.get_int "search_engine.port"
 let pages_dir = Helm_registry.get "search_engine.html_dir"
 
-let interactive_interpretation_choice_TPL = pages_dir ^ "/moogle_chat2.html"
 let moogle_TPL = pages_dir ^ "/moogle.html"
+let choices_TPL = pages_dir ^ "/moogle_chat.html"
 
 let my_own_url =
  let ic = Unix.open_process_in "hostname -f" in
@@ -125,20 +124,30 @@ let query_kind_of_req (req: Http_types.request) =
   | "/elim" -> "Elim"
   | _ -> assert false
 
+  (* given a uri with a query part in input try to find in it a string
+   * "&param_name=..." (where param_name is given). If found its value will be
+   * set to param_value. If not, a trailing "&param_name=param_value" (where
+   * both are given) is added to the input string *)
+let patch_param param_name param_value url =
+  let rex = Pcre.regexp (sprintf "&%s=[^&]*" (Pcre.quote param_name)) in
+  if Pcre.pmatch ~rex url then
+    Pcre.replace ~rex ~templ:(sprintf "%s=%s" param_name param_value) url
+  else
+    sprintf "%s&%s=%s" url param_name param_value
+
 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 interp = try req#param "interp" with Http_types.Param_not_found _ -> "" in
   let page_link anchor page =
     try
       let this = req#param "this" in
       let target =
-        if Pcre.pmatch ~rex:page_RE this then
-          Pcre.replace ~rex:page_RE ~templ:(sprintf "&param.page=%d" page)
-            this
-        else
-          sprintf "%s&param.page=%d" this page
+        (patch_param "param.interp" interp
+           (patch_param "param.page" (string_of_int page)
+              this))
       in
       let target = Pcre.replace ~pat:"&" ~templ:"&amp;" target in
       sprintf "<a href=\"%s\">%s</a>" target anchor
@@ -275,19 +284,23 @@ let exec_action dbd (req: Http_types.request) outchan =
                 req#param "advanced"
               with Http_types.Param_not_found _ -> "no"
             in
+            let query_kind = query_kind_of_req req in
             iter_file
               (fun line ->
                  let processed_line =
                    apply_substs
-                     [tag "ADVANCED", advanced;
-                      tag "INTERPRETATIONS", html_interpretations;
-                      tag "CURRENT_CHOICES", req#param "choices";
-                      tag "EXPRESSION", req#param "expression";
-                      tag "ACTION", string_tail req#path ]
-                      line
+                     [ tag "SEARCH_ENGINE_URL", my_own_url;
+                       tag "ADVANCED", advanced;
+                       tag "INTERPRETATIONS", html_interpretations;
+                       tag "CURRENT_CHOICES", req#param "choices";
+                       tag "EXPRESSION", req#param "expression";
+                       tag "QUERY_KIND", query_kind;
+                       tag "QUERY_SUMMARY", "disambiguation";
+                       tag "ACTION", string_tail req#path ]
+                     line
                  in
                  output_string outchan (processed_line ^ "\n"))
-              interactive_interpretation_choice_TPL;
+              choices_TPL;
             raise Chat_unfinished
 
       let input_or_locate_uri ~title ?id () =