- bugfix use disambiguator metasenv for initial proof status in hint

- use configuration file from /etc
- catch Chat_unfinished
- removed ancient debugging messages

diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml
index bc4cd729a67128de91304c2c5c100c272554e4c6..758d57e0a12199b98e59b98e0335c9404d0820b4 100644 (file)
--- 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 ->