X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FsearchEngine%2FsearchEngine.ml;h=87546b1ffdff61fbdd0a73e93a859aa087427674;hb=ccb56bd6ddeec70a1fb32304aec60a0721d260cc;hp=d327c71bf54a80af3be15d10e543ad5f49d90687;hpb=17a935085d171c7ba4d9894931bfe6c74dc93528;p=helm.git

diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml
index d327c71bf..87546b1ff 100644
--- a/helm/searchEngine/searchEngine.ml
+++ b/helm/searchEngine/searchEngine.ml
@@ -25,8 +25,6 @@
 
 open Printf
 
-module DB = Dbi_mysql
-
 let debug = true
 let debug_print s = if debug then prerr_endline s
 let _ = Http_common.debug := false
@@ -37,6 +35,7 @@ exception Invalid_action of string  (* invalid action for "/search" method *)
 
 let daemon_name = "Moogle"
 let configuration_file = "/projects/helm/etc/moogle.conf.xml" 
+(*let configuration_file = "searchEngine.conf.xml" *)
 
 let placeholders = [
   "EXPRESSION"; "ACTION"; "ADVANCED"; "ADVANCED_CHECKED"; "SIMPLE_CHECKED";
@@ -189,7 +188,7 @@ let send_results results
       output_string outchan (processed_line ^ "\n"))
     moogle_TPL
 
-let exec_action dbh (req: Http_types.request) outchan =
+let exec_action dbd (req: Http_types.request) outchan =
   let term_str = req#param "expression" in
   let (context, metasenv) = ([], []) in
   let id_to_uris_raw = 
@@ -271,14 +270,14 @@ let exec_action dbh (req: Http_types.request) outchan =
   let ast = CicTextualParser2.parse_term (Stream.of_string term_str) in
   let (id_to_uris, metasenv, term) =
     match
-      Disambiguate'.disambiguate_term dbh context metasenv ast id_to_uris
+      Disambiguate'.disambiguate_term dbd context metasenv ast id_to_uris
     with
-    | [id_to_uris,metasenv,term] -> id_to_uris,metasenv,term
+    | [id_to_uris,metasenv,term,_] -> id_to_uris,metasenv,term
     | _ -> assert false
   in
   let uris =
     match req#path with
-    | "/match" -> MetadataQuery.match_term ~dbh term
+    | "/match" -> MetadataQuery.match_term ~dbd term
     | "/hint" ->
         let status = ProofEngineTypes.initial_status term metasenv in
         let intros = PrimitiveTactics.intros_tac () in
@@ -286,7 +285,7 @@ let exec_action dbh (req: Http_types.request) outchan =
         (match subgoals with
         | proof, [goal] ->
             let (uri,metasenv,bo,ty) = proof in
-            List.map fst (MetadataQuery.hint ~dbh (proof, goal))
+            List.map fst (MetadataQuery.hint ~dbd (proof, goal))
         | _ -> assert false)
     | "/elim" ->
         let uri =
@@ -295,12 +294,12 @@ let exec_action dbh (req: Http_types.request) outchan =
               UriManager.string_of_uriref (uri, [typeno])
           | _ -> assert false
         in
-        MetadataQuery.elim ~dbh uri
+        MetadataQuery.elim ~dbd uri
     | _ -> assert false
   in
   send_results ~id_to_uris (`Results uris) req outchan
 
-let callback dbh (req: Http_types.request) outchan =
+let callback dbd (req: Http_types.request) outchan =
   try
     debug_print (sprintf "Received request: %s" req#path);
     (match req#path with
@@ -346,11 +345,11 @@ let callback dbh (req: Http_types.request) outchan =
         if expression = "" then
           send_results (`Results []) req outchan
         else
-          let results = MetadataQuery.locate ~dbh expression in
+          let results = MetadataQuery.locate ~dbd expression in
           send_results (`Results results) req outchan
     | "/hint"
     | "/elim"
-    | "/match" -> exec_action dbh req outchan
+    | "/match" -> exec_action dbd req outchan
     | invalid_request ->
         Http_daemon.respond_error ~code:(`Status (`Client_error `Bad_request))
           outchan);
@@ -359,7 +358,7 @@ let callback dbh (req: Http_types.request) outchan =
   | Chat_unfinished -> ()
   | Http_types.Param_not_found attr_name ->
       bad_request (sprintf "Parameter '%s' is missing" attr_name) outchan
-  | CicTextualParser2.Parse_error msg ->
+  | CicTextualParser2.Parse_error (_, msg) ->
       send_results (`Error (MooglePp.pp_error "Parse_error" msg)) req outchan
   | Unbound_identifier id ->
       send_results (`Error (MooglePp.pp_error "Unbound identifier" id)) req
@@ -376,10 +375,13 @@ let _ =
   printf "HTML directory is %s\n" pages_dir;
   flush stdout;
   Unix.putenv "http_proxy" "";
-  let dbh =
-    new DB.connection ~host:(Helm_registry.get "db.host")
-      ~user:(Helm_registry.get "db.user") (Helm_registry.get "db.database")
+  let dbd =
+    Mysql.quick_connect
+      ~host:(Helm_registry.get "db.host")
+      ~database:(Helm_registry.get "db.database")
+      ~user:(Helm_registry.get "db.user")
+      ()
   in
-  Http_daemon.start' ~port (callback dbh);
+  Http_daemon.start' ~port (callback dbd);
   printf "%s is terminating, bye!\n" daemon_name