From: Stefano Zacchiroli Date: Tue, 22 Jun 2004 15:33:17 +0000 (+0000) Subject: ugliness changes: X-Git-Tag: pre_subst_in_kernel~18 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=aeac77539da374b9c9a0f3aae1c7b43963c9dab9;p=helm.git ugliness changes: - more google like look and feel for query results - exceptions are no longer rendered in

elements but pretty printed inside the standard moogle HTML template - advanced search status is now rememberd between searches - added results count - added result type feedback in results page --- diff --git a/helm/searchEngine/html/moogle.html b/helm/searchEngine/html/moogle.html index f608b9d28..dd6429634 100644 --- a/helm/searchEngine/html/moogle.html +++ b/helm/searchEngine/html/moogle.html @@ -2,6 +2,19 @@ Moogle + @@ -36,10 +49,10 @@ - - Simple search - - Advanced search + + Simple search + + Advanced search @@ -47,7 +60,6 @@ -
@RESULTS@ diff --git a/helm/searchEngine/html/moogle_help.html b/helm/searchEngine/html/moogle_help.html index e6252cc28..22bb5412c 100644 --- a/helm/searchEngine/html/moogle_help.html +++ b/helm/searchEngine/html/moogle_help.html @@ -1,85 +1 @@ - - - -Moogle_help - - - - - - - - - - - - - - - - - - - - - - - - -
- - - - - - - - - Help
- Input Syntax - -
- - - Simple search - - Advanced search - -
- -
- -
- -
hint -
-
-
- -
ccccccccccccc
-
- -
- - Locate and display an object by its short name.
- For instance - locating the identifier "nat" gives you back the definition of - natural numbers, and locating "plus" returns several (axiomatic and - concrete) definitions of the sum. -
- -
- - Given a closed statement G of the form -
- \forall x₁:T₁...x_n:T_n.body - - returns all theorems in the library whose conclusion is a generalization - of body, that is all theorems which can be used (as a last step) to prove G - (for tecnical reasons, the actual result may be a superset of - the expected one). -
- - - - +

Coming soon!
diff --git a/helm/searchEngine/html/moogle_init.html b/helm/searchEngine/html/moogle_init.html index af4c26c26..feddb620c 100644 --- a/helm/searchEngine/html/moogle_init.html +++ b/helm/searchEngine/html/moogle_init.html @@ -2,6 +2,9 @@ Moogle + diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml index e52d0aa35..1f45fe67c 100644 --- a/helm/searchEngine/searchEngine.ml +++ b/helm/searchEngine/searchEngine.ml @@ -1,4 +1,4 @@ -(* Copyright (C) 2002, HELM Team. +(* Copyright (C) 2002-2004, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -28,16 +28,16 @@ module U = MQGUtil module G = MQueryGenerator module C = MQIConn -open Http_types ;; +open Http_types -let debug = true;; -let debug_print s = if debug then prerr_endline s;; -Http_common.debug := true;; -(* Http_common.debug := true;; ) +let debug = true +let debug_print s = if debug then prerr_endline s +let _ = Http_common.debug := true +( let _ = Http_common.debug := false *) -open Printf;; +open Printf -let daemon_name = "Search Engine";; +let daemon_name = "Search Engine" let string_tail s = let len = String.length s in @@ -47,45 +47,40 @@ let string_tail s = let _ = let configuration_file = "/projects/helm/etc/searchEngine.conf.xml" in Helm_registry.load_from configuration_file -;; -let port = Helm_registry.get_int "search_engine.port";; +let port = Helm_registry.get_int "search_engine.port" -let pages_dir = Helm_registry.get "search_engine.html_dir";; +let pages_dir = Helm_registry.get "search_engine.html_dir" (** accepted HTTP servers for ask_uwobo method forwarding ) -let valid_servers= Helm_registry.get_string_list "search_engine.valid_servers";; +let valid_servers= Helm_registry.get_string_list "search_engine.valid_servers" -let interactive_user_uri_choice_TPL = pages_dir ^ "/moogle_chat1.html";; -let interactive_interpretation_choice_TPL = pages_dir ^ "/moogle_chat2.html";; -let constraints_choice_TPL = pages_dir ^ "/moogle_constraints_choice.html";; -( let final_results_TPL = pages_dir ^ "/templateambigpdq3.html";; ) -let start_TPL = pages_dir ^ "/moogle.html";; -let final_results_TPL = pages_dir ^ "/moogle.html";; +let interactive_user_uri_choice_TPL = pages_dir ^ "/moogle_chat1.html" +let interactive_interpretation_choice_TPL = pages_dir ^ "/moogle_chat2.html" +let constraints_choice_TPL = pages_dir ^ "/moogle_constraints_choice.html" +let moogle_TPL = pages_dir ^ "/moogle.html" let my_own_url = let ic = Unix.open_process_in "hostname -f" in let hostname = input_line ic in ignore (Unix.close_process_in ic); sprintf "http://%s:%d" hostname port -;; exception Chat_unfinished exception Invalid_action of string ( invalid action for "/search" method ) +exception Unbound_identifier of string let javascript_quote s = let rex = Pcre.regexp "'" in let rex' = Pcre.regexp "\"" in Pcre.replace ~rex ~templ:"\\'" (Pcre.replace ~rex:rex' ~templ:"\\\"" s) -;; ( build a bool from a 1-character-string ) let bool_of_string' = function | "0" -> false | "1" -> true | s -> failwith ("Can't parse a boolean from string: " ^ s) -;; ( build an int option from a string ) let int_of_string' = function @@ -95,7 +90,6 @@ let int_of_string' = function Some (int_of_string s) with Failure "int_of_string" -> failwith ("Can't parse an int option from string: " ^ s) -;; ( HTML pretty printers for mquery_generator types *) @@ -108,22 +102,27 @@ let html_of_r_obj (pos, uri) = (U.text_of_depth pos "") else "") -;; let html_of_r_rel pos = sprintf "%s" (U.text_of_position (pos:>T.full_position)) (U.text_of_depth (pos:>T.full_position) "") -;; let html_of_r_sort (pos, sort) = sprintf "%s%s" (U.text_of_sort sort) (U.text_of_position (pos:>T.full_position)) (U.text_of_depth (pos:>T.full_position) "") -;; + +let query_of_req (req: Http_types.request) = + match req#path with + | "/elim" -> "Elim" + | "/match" -> "Match" + | "/hint" -> "Hint" + | "/locate" -> "Locate" + | _ -> assert false (** pretty print a MathQL query result to an HELM theory file *) -let theory_of_result result = +let theory_of_result req result = let results_no = List.length result in if results_no > 0 then let mode = if results_no > 10 then "linkonly" else "typeonly" in @@ -132,17 +131,42 @@ let theory_of_result result = List.fold_right (fun uri i -> decr idx ; - "" ^ string_of_int !idx ^ "." ^ i - ) result "" + sprintf + " + %d. + + %s" + !idx uri mode i) + result "" in - "Query Results:" ^ results ^ "
" + sprintf + "
+ + + + + +
%s %d result%s found
+
+
+
+ %s
+
" + (query_of_req req) + results_no (if results_no > 1 then "s" else "") results else - "Query Results:
No results found!
" -;; - -let pp_result result = - "\nQuery Results\n" ^ theory_of_result result ^ "" -;; + "
no results found
" + +let pp_result req result = + sprintf + " + + Query results + + + %s + " + (theory_of_result req result) (** chain application of Pcre substitutions *) let rec apply_substs substs line = @@ -164,17 +188,15 @@ let fold_file f init fname = (** iter like function on files ) let iter_file f = fold_file (fun _ line -> f line) () -let (expression_tag_RE, - action_tag_RE, - advanced_tag_RE, +let (expression_tag_RE, action_tag_RE, advanced_tag_RE, + advanced_checked_RE, simple_checked_RE, title_tag_RE, no_choices_tag_RE, current_choices_tag_RE, choices_tag_RE, msg_tag_RE, id_to_uris_RE, id_RE, iden_tag_RE, interpretations_RE, interpretations_labels_RE, results_RE, new_aliases_RE, form_RE, variables_initialization_RE, search_engine_url_RE) = - (Pcre.regexp "@EXPRESSION@", - Pcre.regexp "@ACTION@", - Pcre.regexp "@ADVANCED@", + (Pcre.regexp "@EXPRESSION@", Pcre.regexp "@ACTION@", Pcre.regexp "@ADVANCED@", + Pcre.regexp "@ADVANCED_CHECKED@", Pcre.regexp "@SIMPLE_CHECKED@", Pcre.regexp "@TITLE@", Pcre.regexp "@NO_CHOICES@", Pcre.regexp "@CURRENT_CHOICES@", Pcre.regexp "@CHOICES@", Pcre.regexp "@MSG@", @@ -184,14 +206,15 @@ let (expression_tag_RE, Pcre.regexp "@VARIABLES_INITIALIZATION@", Pcre.regexp "@SEARCH_ENGINE_URL@") let server_and_port_url_RE = Pcre.regexp "^http://([^/]+)/.$" -let pp_error = sprintf "
Error: %s
";; +(* let pp_error = sprintf "
Error: %s
" ) +let pp_error title msg = + sprintf "
%s: %s
" title msg let bad_request body outchan = Http_daemon.respond_error ~code:(`Status (`Client_error `Bad_request)) ~body outchan -;; -let contype = "Content-Type", "text/html";; +let contype = "Content-Type", "text/html" ( SEARCH ENGINE functions ) @@ -214,7 +237,6 @@ let get_constraints term = (Some CGMatchConclusion.universe), (List.nth list_of_must block, [], []), (Some only, None, None) | _ -> assert false -;; ( format: @@ -287,7 +309,6 @@ let add_user_constraints ~constraints in (must', only') | _ -> failwith ("Can't parse constraint string: " ^ constraints) -in let send_results results ?(id_to_uris = DisambiguatingParser.EnvironmentP3.of_string "") @@ -296,9 +317,14 @@ 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 results_string = + match results with + | `Results r -> theory_of_result req r + | `Error msg -> msg + in let subst = (search_engine_url_RE, my_own_url) :: - (results_RE, theory_of_result results):: + (results_RE, results_string):: (advanced_tag_RE, req#param "advanced"):: (expression_tag_RE, req#param "expression"):: (List.map @@ -306,23 +332,28 @@ let send_results results let key' = (Pcre.extract ~pat:"param\\.(.)" key).(1) in Pcre.regexp ("@" ^ key' ^ "@"), value) (List.filter - (fun (key,_) as p-> Pcre.pmatch ~pat:"^param\\." key) - req#params)) - in - iter_file - (fun line -> - let new_aliases = - DisambiguatingParser.EnvironmentP3.to_string id_to_uris - in - let processed_line = - apply_substs - ( CSC: Bug here: this is a string, not an array! ) - ((new_aliases_RE, "'" ^ javascript_quote new_aliases ^ "'")::subst) - line - in - output_string outchan (processed_line ^ "\n")) - final_results_TPL -in + (fun (key,_) as p-> Pcre.pmatch ~pat:"^param\\." key) + req#params)) @ + (if req#param "advanced" = "no" then + [ simple_checked_RE, "checked='true'"; + advanced_checked_RE, "" ] + else + [ simple_checked_RE, ""; + advanced_checked_RE, "checked='true'" ]) + in + iter_file + (fun line -> + let new_aliases = + DisambiguatingParser.EnvironmentP3.to_string id_to_uris + in + let processed_line = + apply_substs + ( CSC: Bug here: this is a string, not an array! ) + ((new_aliases_RE, "'" ^ javascript_quote new_aliases ^ "'")::subst) + line + in + output_string outchan (processed_line ^ "\n")) + moogle_TPL let exec_action mqi_handle (req: Http_types.request) outchan = let term_string = req#param "expression" in @@ -453,7 +484,9 @@ let exec_action mqi_handle (req: Http_types.request) outchan = raise Chat_unfinished let input_or_locate_uri ~title ?id () = - assert false + match id with + | Some id -> raise (Unbound_identifier id) + | None -> assert false end in @@ -482,7 +515,7 @@ let exec_action mqi_handle (req: Http_types.request) outchan = | _ -> assert false in let results = List.map snd (Match_concl.cmatch dbd term') in - send_results results ~id_to_uris:id_to_uris' req outchan + send_results (`Results results) ~id_to_uris:id_to_uris' req outchan else let must'', only' = (try @@ -568,8 +601,8 @@ let exec_action mqi_handle (req: Http_types.request) outchan = G.query_of_constraints universe must'' only' in let results = MQueryInterpreter.execute mqi_handle query in - send_results (List.map fst results) ~id_to_uris:id_to_uris' req outchan -in + send_results (`Results (List.map fst results)) + ~id_to_uris:id_to_uris' req outchan ( HTTP DAEMON CALLBACK ) @@ -577,7 +610,6 @@ let build_dynamic_uri url params = let p = String.concat "&" (List.map (fun (key,value) -> (key ^ "=" ^ (Netencoding.Url.encode value))) params) in url ^ "?" ^ p -in let build_uwobo_request (req: Http_types.request) outchan = prerr_endline ("ECCOLO: " ^ req#param "param.SEARCH_ENGINE_URL"); @@ -598,10 +630,8 @@ let build_uwobo_request (req: Http_types.request) outchan = outchan else Http_daemon.respond - ~body:(pp_error ("Untrusted UWOBO server: " ^ server_and_port ^ - (String.concat "\n" valid_servers))) + ~body:(pp_error "Untrusted UWOBO server" server_and_port) outchan -in let proxy url outchan = let server_and_port = @@ -614,9 +644,8 @@ let proxy url outchan = outchan else Http_daemon.respond - ~body:(pp_error ("Untrusted UWOBO server: " ^ server_and_port)) + ~body:(pp_error "Untrusted UWOBO server" server_and_port) outchan -in let callback mqi_handle (req: Http_types.request) outchan = try @@ -632,28 +661,28 @@ let callback mqi_handle (req: Http_types.request) outchan = (Pcre.replace ~pat:"^\\s" initial_expression) in if expression = "" then - send_results [] req outchan + send_results (`Results []) req outchan else let results = let query = G.locate expression in MQueryInterpreter.execute mqi_handle query in - send_results (List.map fst results) req outchan + send_results (`Results (List.map fst results)) req outchan | "/execute" -> let query_string = req#param "query" in let lexbuf = Lexing.from_string query_string in let query = MQueryUtil.query_of_text lexbuf in let result = MQueryInterpreter.execute mqi_handle query in - let result_string = pp_result (List.map fst result) in + let result_string = pp_result req (List.map fst result) in Http_daemon.respond ~body:result_string ~headers:[contype] outchan -(* Http_daemon.respond ~headers:[contype] ~body:(pp_result result) outchan ) +( Http_daemon.respond ~headers:[contype] ~body:(pp_result req result) outchan ) | "/unreferred" -> let target = req#param "target" in let source = req#param "source" in let query = G.unreferred target source in let result = MQueryInterpreter.execute mqi_handle query in Http_daemon.respond ~headers:[contype] - ~body:(pp_result (List.map fst result)) outchan + ~body:(pp_result req (List.map fst result)) outchan | "/getpage" -> ( TODO implement "is_permitted" ) let _ = prerr_endline @@ -699,10 +728,7 @@ let callback mqi_handle (req: Http_types.request) outchan = | page -> Http_daemon.respond_forbidden ~url:page outchan)) ( OLD | "/ask_uwobo" -> proxy (req#param "url") outchan *) | "/ask_uwobo" -> build_uwobo_request req outchan - | "/hint" - | "/match" - | "/elim" -> - exec_action mqi_handle req outchan + | "/hint" | "/match" | "/elim" -> exec_action mqi_handle req outchan | invalid_request -> Http_daemon.respond_error ~code:(`Status (`Client_error `Bad_request)) outchan); @@ -711,17 +737,24 @@ let callback mqi_handle (req: Http_types.request) outchan = | Chat_unfinished -> prerr_endline "Chat unfinished, Try again!" | Http_types.Param_not_found attr_name -> bad_request (sprintf "Parameter '%s' is missing" attr_name) outchan - | exc -> - let msg = sprintf "Uncaught exception: %s" (Printexc.to_string exc) in - debug_print msg ; - Http_daemon.respond ~body:(pp_error msg) outchan -in -printf "%s started and listening on port %d\n" daemon_name port; -printf "Current directory is %s\n" (Sys.getcwd ()); -printf "HTML directory is %s\n" pages_dir; -flush stdout; -Unix.putenv "http_proxy" ""; -let mqi_handle = C.init ~log:debug_print () in -Http_daemon.start' ~port (callback mqi_handle); -C.close mqi_handle; -printf "%s is terminating, bye!\n" daemon_name + | CicTextualParser2.Parse_error msg -> + send_results (`Error (pp_error "Parse_error" msg)) req outchan + | Unbound_identifier id -> + send_results (`Error (pp_error "Unbound identifier" id)) req outchan + | exn -> + let exn_string = Printexc.to_string exn in + debug_print exn_string; + let msg = pp_error "Uncaught exception" exn_string in + send_results (`Error msg) req outchan + +let _ = + printf "%s started and listening on port %d\n" daemon_name port; + printf "Current directory is %s\n" (Sys.getcwd ()); + printf "HTML directory is %s\n" pages_dir; + flush stdout; + Unix.putenv "http_proxy" ""; + let mqi_handle = C.init ~log:debug_print () in + Http_daemon.start' ~port (callback mqi_handle); + C.close mqi_handle; + printf "%s is terminating, bye!\n" daemon_name +