New module HMysql (to abstract over Mysql and make profiling easier).

diff --git a/helm/matita/matitaDb.ml b/helm/matita/matitaDb.ml
index b5b64d46f1d958c7d9c02a48a099253bb3137176..75d0f67e0e2b12985769b7dc4c59fcfe5bd12a36 100644 (file)
--- a/helm/matita/matitaDb.ml
+++ b/helm/matita/matitaDb.ml
@@ -27,7 +27,7 @@ open Printf ;;
 
 let instance =
   let dbd = lazy (
-    Mysql.quick_connect
+    HMysql.quick_connect
       ~host:(Helm_registry.get "db.host")
       ~user:(Helm_registry.get "db.user")
       ~database:(Helm_registry.get "db.database")
@@ -58,7 +58,7 @@ let clean_owner_environment () =
     try
       MetadataDb.clean ~dbd
     with Mysql.Error _ as exn ->
-      match Mysql.errno dbd with 
+      match HMysql.errno dbd with 
       | Mysql.No_such_table -> []
       | _ -> raise exn
   in
@@ -74,9 +74,9 @@ let clean_owner_environment () =
     owned_uris;
   List.iter (fun statement -> 
     try
-      ignore (Mysql.exec dbd statement)
+      ignore (HMysql.exec dbd statement)
     with Mysql.Error _ as exn ->
-      match Mysql.errno dbd with 
+      match HMysql.errno dbd with 
       | Mysql.Bad_table_error 
       | Mysql.No_such_index | Mysql.No_such_table -> () 
       | _ -> raise exn
@@ -99,10 +99,10 @@ let create_owner_environment () =
   in
   List.iter (fun statement -> 
     try
-      ignore (Mysql.exec dbd statement)
+      ignore (HMysql.exec dbd statement)
     with
       exn -> 
-         let status = Mysql.status dbd in
+         let status = HMysql.status dbd in
          match status with 
          | Mysql.StatusError Mysql.Table_exists_error -> ()
          | Mysql.StatusError Mysql.Dup_keyname -> ()
@@ -129,11 +129,11 @@ let remove_uri uri =
   let dbd = instance () in
   let suri = UriManager.string_of_uri uri in 
   let query table suri = sprintf 
-    "DELETE FROM %s WHERE source LIKE '%s%%'" table (Mysql.escape suri)
+    "DELETE FROM %s WHERE source LIKE '%s%%'" table (HMysql.escape suri)
   in
   List.iter (fun t -> 
     try 
-      ignore (Mysql.exec dbd (query t suri))
+      ignore (HMysql.exec dbd (query t suri))
     with
       exn -> raise exn (* no errors should be accepted *)
     )
@@ -141,12 +141,12 @@ let remove_uri uri =
   (* and now the debug job *)  
   let dbg_q = 
     sprintf "SELECT source FROM %s WHERE h_occurrence LIKE '%s%%'" obj_tbl
-    (Mysql.escape suri)
+    (HMysql.escape suri)
   in
   try 
-    let rc = Mysql.exec dbd dbg_q in
+    let rc = HMysql.exec dbd dbg_q in
     let l = ref [] in
-    Mysql.iter rc (fun a -> match a.(0) with None ->()|Some a -> l := a:: !l);
+    HMysql.iter rc (fun a -> match a.(0) with None ->()|Some a -> l := a:: !l);
     let l = List.sort Pervasives.compare !l in
     MatitaMisc.list_uniq l
   with
@@ -157,10 +157,10 @@ let xpointers_of_ind uri =
   let name_tbl =  MetadataTypes.name_tbl () in
   let query = sprintf 
     "SELECT source FROM %s WHERE source LIKE '%s#xpointer%%'" name_tbl 
-      (Mysql.escape (UriManager.string_of_uri uri))
+      (HMysql.escape (UriManager.string_of_uri uri))
   in
-  let rc = Mysql.exec dbd query in
+  let rc = HMysql.exec dbd query in
   let l = ref [] in
-  Mysql.iter rc (fun a ->  match a.(0) with None ->()|Some a -> l := a:: !l);
+  HMysql.iter rc (fun a ->  match a.(0) with None ->()|Some a -> l := a:: !l);
   List.map UriManager.uri_of_string !l
 

diff --git a/helm/matita/matitaDb.mli b/helm/matita/matitaDb.mli
index 09eff29893318b241d8abd6b8b0fd15a9da6374d..0d5811eba7fbfdc58a879c54c9a3f2e5da8696f0 100644 (file)
--- a/helm/matita/matitaDb.mli
+++ b/helm/matita/matitaDb.mli
@@ -23,7 +23,7 @@
  * http://helm.cs.unibo.it/
  *)
 
-val instance: unit -> Mysql.dbd
+val instance: unit -> HMysql.dbd
 
 val create_owner_environment: unit -> unit
 val clean_owner_environment: unit -> unit

diff --git a/helm/matita/matitacleanLib.ml b/helm/matita/matitacleanLib.ml
index dafd8097cbeb69d66450562c62601587dd35b014..a263a526fd7e05a65855b3413a8eecef3818b630 100644 (file)
--- a/helm/matita/matitacleanLib.ml
+++ b/helm/matita/matitacleanLib.ml
@@ -47,15 +47,15 @@ let one_step_depend suri =
       Hashtbl.add cache_of_processed_baseuri buri true;
       let query = 
         let buri = buri ^ "/" in 
-        let buri = Mysql.escape buri in
+        let buri = HMysql.escape buri in
         let obj_tbl = MetadataTypes.obj_tbl () in
         Printf.sprintf 
           "SELECT source, h_occurrence FROM %s WHERE h_occurrence LIKE '%s%%'" obj_tbl buri
       in
       try 
-        let rc = Mysql.exec (MatitaDb.instance ()) query in
+        let rc = HMysql.exec (MatitaDb.instance ()) query in
         let l = ref [] in
-        Mysql.iter rc (
+        HMysql.iter rc (
           fun row -> 
             match row.(0), row.(1) with 
             | Some uri, Some occ when Filename.dirname occ = buri -> 
@@ -152,7 +152,7 @@ let clean_baseuris ?(verbose=true) buris =
     cleaned_no := 0;
     List.iter
      (function table ->
-       ignore (Mysql.exec (MatitaDb.instance ()) ("OPTIMIZE TABLE " ^ table)))
+       ignore (HMysql.exec (MatitaDb.instance ()) ("OPTIMIZE TABLE " ^ table)))
      [MetadataTypes.name_tbl (); MetadataTypes.rel_tbl ();
       MetadataTypes.sort_tbl (); MetadataTypes.obj_tbl();
       MetadataTypes.count_tbl()]