no longer use Dbi module but directly use Mysql module since it's 13

[helm.git] / helm / gTopLevel / gTopLevel.ml

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 82317959a12b576739672dcb797d5ee0083dab83..b6aa28caea1655e9569d1274188be940841580e5 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -40,16 +40,12 @@ let warning s = prerr_endline ("W: " ^ s)
 
 open Printf
 
-(* DEBUGGING *)
-
 module MQI  = MQueryInterpreter
 module MQIC = MQIConn
 module MQGT = MQGTypes
 module MQGU = MQGUtil
 module MQG  = MQueryGenerator
 
-module DB = Dbi_mysql
-
 (* first of all let's initialize the Helm_registry *)
 let _ =
  let configuration_file = "gTopLevel.conf.xml" in
@@ -62,9 +58,14 @@ let _ =
 
 (* GLOBAL CONSTANTS *)
 
-let mqi_debug_fun s = debug_print ~level:2 s
-let mqi_handle = MQIC.init_if_connected ~log:mqi_debug_fun ()
-let dbh = new DB.connection ~host:"mowgli.cs.unibo.it" ~user:"helm" "mowgli"
+let mqi_handle = MQIC.init_if_connected ()
+
+let dbd =
+  Mysql.quick_connect
+    ~host:(Helm_registry.get "db.host")
+    ~user:(Helm_registry.get "db.user")
+    ~database:(Helm_registry.get "db.database")
+    ()
 
 let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";;
 
@@ -649,7 +650,7 @@ module InvokeTacticsCallbacks =
   let decompose_uris_choice_callback = decompose_uris_choice_callback
   let mk_fresh_name_callback = mk_fresh_name_callback
   let mqi_handle = mqi_handle
-  let dbh = dbh
+  let dbd = dbd
  end
 ;;
 module InvokeTactics' = InvokeTactics.Make (InvokeTacticsCallbacks);;
@@ -913,7 +914,7 @@ let user_uri_choice ~title ~msg uris =
 ;;
 
 let locate_callback id =
- let uris = MetadataQuery.locate ~dbh id in
+ let uris = MetadataQuery.locate ~dbd id in
   HelmLogger.log (`Msg (`T ("Locate Query: " ^ id))) ;
   HelmLogger.log (`Msg (`T "Result:")) ;
   List.iter (fun uri -> HelmLogger.log (`Msg (`T uri))) uris;
@@ -1185,7 +1186,7 @@ let new_inductive () =
         ~packing:(vbox#pack ~expand:true ~padding:0) () in
       let newinputt =
        TermEditor'.term_editor
-        ~dbh
+        ~dbd
         ~width:400 ~height:20 ~packing:scrolled_window#add 
         ~share_environment_with:inputt ()
         ~isnotempty_callback:
@@ -1297,7 +1298,7 @@ let new_inductive () =
         ~packing:(vbox#pack ~expand:true ~padding:0) () in
       let newinputt =
        TermEditor'.term_editor
-        ~dbh
+        ~dbd
         ~width:400 ~height:20 ~packing:scrolled_window#add
         ~share_environment_with:inputt ()
         ~isnotempty_callback:
@@ -1443,7 +1444,7 @@ let new_proof () =
  (* moved here to have visibility of the ok button *)
  let newinputt =
   TermEditor'.term_editor
-   ~dbh
+   ~dbd
    ~width:400 ~height:100 ~packing:scrolled_window#add
    ~share_environment_with:inputt ()
    ~isnotempty_callback:
@@ -2054,7 +2055,7 @@ let searchPattern () =
      match !ProofEngine.goal with
       | None -> ()
       | Some metano ->
-         let uris' = List.map fst (MetadataQuery.hint ~dbh (proof, metano)) in
+         let uris' = List.map fst (MetadataQuery.hint ~dbd (proof, metano)) in
          let uri' =
           user_uri_choice ~title:"Ambiguous input."
           ~msg: "Many lemmas can be successfully applied. Please, choose one:"
@@ -2783,7 +2784,7 @@ class rendering_window output (notebook : notebook) =
    ~packing:frame#add () in
  let inputt =
   TermEditor'.term_editor
-   ~dbh
+   ~dbd
    ~width:400 ~height:100 ~packing:scrolled_window1#add ()
    ~isnotempty_callback:
     (function b ->