From 9826bf0a143ca0563cb4b29a6bdfe1df7efd2a04 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 20 Sep 2005 16:30:28 +0000 Subject: [PATCH] More profiling code inserted. --- helm/matita/matitaSync.ml | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) 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 -- 2.39.2