From: Stefano Zacchiroli 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