From: Stefano Zacchiroli 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 "" n + let choice_of_interp interp = + sprintf "\n%s\n
" + (String.concat "\n" + (List.map + (fun (k, v) -> + sprintf "%s%s" k v) + interp)) in - let text interp = - String.concat "
" - (List.map - (fun (id, value) -> sprintf "%s = %s" id value) - interp) - in - let rec aux n = function - | [] -> [] - | interp::tl -> ((radio_button n)^(text interp))::(aux (n+1) tl) - in - String.concat "
" (aux 0 interps) + let interp_no = ref ~-1 in + sprintf "\n%s\n
" + (String.concat "\n" + (List.map + (fun interp -> + sprintf " + + + + %s + " + (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 + * "¶m_name=..." (where param_name is given). If found its value will be + * set to param_value. If not, a trailing "¶m_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 "¶m.page=%d" page) - this - else - sprintf "%s¶m.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:"&" target in sprintf "%s" 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 () =