More profiling code inserted.

[helm.git] / helm / matita / matitaSync.ml

diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index d3ae5fdc9deee3a8ccb4f225b99c177e97bc220c..84d107f30d599596549627b94b19ae2075bda9d6 100644 (file)
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -154,6 +154,16 @@ let typecheck_obj =
  let profiler = CicUtil.profile "add_obj.typecheck_obj" in
   fun uri obj -> profiler.CicUtil.profile (CicTypeChecker.typecheck_obj uri) obj
 
+let index_obj =
+ let profiler = CicUtil.profile "add_obj.index_obj" in
+  fun ~dbd ~uri ->
+   profiler.CicUtil.profile (fun uri -> MetadataDb.index_obj ~dbd ~uri) uri
+
+let save_object_to_disk =
+ let profiler = CicUtil.profile "add_obj.save_object_to_disk" in
+  fun status uri obj ->
+   profiler.CicUtil.profile (save_object_to_disk status uri) obj
+
 let add_obj uri obj status =
   let dbd = MatitaDb.instance () in
   let suri = UriManager.string_of_uri uri in
@@ -162,7 +172,7 @@ let add_obj uri obj status =
   else begin
     typecheck_obj uri obj; (* 1 *)
     try 
-      MetadataDb.index_obj ~dbd ~uri; (* 2 must be in the env *)
+      index_obj ~dbd ~uri; (* 2 must be in the env *)
       try
         let new_stuff = save_object_to_disk status uri obj in (* 3 *)
         try