ported to Mysql native connection

diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml
index d327c71bf54a80af3be15d10e543ad5f49d90687..111c9b804400d4f555c105b3bbfcd82dc0223258 100644 (file)
--- a/helm/searchEngine/searchEngine.ml
+++ b/helm/searchEngine/searchEngine.ml
@@ -189,7 +189,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 +271,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
     | _ -> 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 +286,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 +295,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 +346,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);
@@ -376,10 +376,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