From 1ca4ec397bd2def234b380aceccd3afd4201fa2e Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 25 Oct 2004 15:27:08 +0000 Subject: [PATCH] - bugfix use disambiguator metasenv for initial proof status in hint - use configuration file from /etc - catch Chat_unfinished - removed ancient debugging messages --- helm/searchEngine/searchEngine.ml | 16 +++++++--------- 1 file changed, 7 insertions(+), 9 deletions(-) diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml index bc4cd729a..758d57e0a 100644 --- a/helm/searchEngine/searchEngine.ml +++ b/helm/searchEngine/searchEngine.ml @@ -36,7 +36,7 @@ exception Unbound_identifier of string exception Invalid_action of string (* invalid action for "/search" method *) let daemon_name = "Moogle" -let configuration_file = "searchEngine.conf.xml" +let configuration_file = "/projects/helm/etc/moogle.conf.xml" let expression_tag_RE = Pcre.regexp "@EXPRESSION@" let action_tag_RE = Pcre.regexp "@ACTION@" @@ -55,10 +55,7 @@ let interpretations_RE = Pcre.regexp "@INTERPRETATIONS@" let interpretations_labels_RE = Pcre.regexp "@INTERPRETATIONS_LABELS@" let results_RE = Pcre.regexp "@RESULTS@" let new_aliases_RE = Pcre.regexp "@NEW_ALIASES@" -let form_RE = Pcre.regexp "@FORM@" -let variables_initialization_RE = Pcre.regexp "@VARIABLES_INITIALIZATION@" let search_engine_url_RE = Pcre.regexp "@SEARCH_ENGINE_URL@" -let server_and_port_url_RE = Pcre.regexp "^http://([^/]+)/.*$" (* First of all we load the configuration *) let _ = Helm_registry.load_from configuration_file @@ -129,9 +126,9 @@ let send_results results in let subst = (search_engine_url_RE, my_own_url) :: - (results_RE, results_string):: - (advanced_tag_RE, req#param "advanced"):: - (expression_tag_RE, req#param "expression"):: + (results_RE, results_string) :: + (advanced_tag_RE, req#param "advanced") :: + (expression_tag_RE, req#param "expression") :: add_param_substs req#params @ (if req#param "advanced" = "no" then [ simple_checked_RE, "checked='true'"; @@ -204,7 +201,7 @@ let exec_action dbh (req: Http_types.request) outchan = let interactive_interpretation_choice interpretations = match interpretation_choices with - | Some l -> prerr_endline "CARRAMBA" ; l + | Some l -> l | None -> let html_interpretations = MooglePp.html_of_interpretations interpretations @@ -245,7 +242,7 @@ let exec_action dbh (req: Http_types.request) outchan = match req#path with | "/match" -> MetadataQuery.match_term ~dbh term | "/hint" -> - let status = ProofEngineTypes.initial_status term [] in + let status = ProofEngineTypes.initial_status term metasenv in let intros = PrimitiveTactics.intros_tac () in let subgoals = ProofEngineTypes.apply_tactic intros status in (match subgoals with @@ -322,6 +319,7 @@ let callback dbh (req: Http_types.request) outchan = outchan); debug_print (sprintf "%s done!" req#path) with + | Chat_unfinished -> () | Http_types.Param_not_found attr_name -> bad_request (sprintf "Parameter '%s' is missing" attr_name) outchan | CicTextualParser2.Parse_error msg -> -- 2.39.2