From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 18 Nov 2004 13:45:18 +0000 (+0000)
Subject: ported to Mysql native connection
X-Git-Tag: PRE_UNIVERSES~24
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9e3da80b505169515fafcbe3ef2438ceb645e35a;p=helm.git

ported to Mysql native connection
---

diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml
index d327c71bf..111c9b804 100644
--- 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