From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 20 Sep 2005 16:30:28 +0000 (+0000)
Subject: More profiling code inserted.
X-Git-Tag: LAST_BEFORE_NEW~76
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9826bf0a143ca0563cb4b29a6bdfe1df7efd2a04;p=helm.git

More profiling code inserted.
---

diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index d3ae5fdc9..84d107f30 100644
--- 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