From: Claudio Sacerdoti Coen Date: Mon, 19 Sep 2005 15:28:59 +0000 (+0000) Subject: More profiling code. X-Git-Tag: LAST_BEFORE_NEW~93 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c9d86ce2c1da11897768511f39f995051562dde0;p=helm.git More profiling code. --- diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml index 6662b7d6e..d3ae5fdc9 100644 --- a/helm/matita/matitaSync.ml +++ b/helm/matita/matitaSync.ml @@ -43,7 +43,7 @@ let alias_diff ~from status = status.aliases Map.empty let alias_diff = - let profiler = CicUtil.profile "accusato" in + let profiler = CicUtil.profile "alias_diff (conteggiato anche in include)" in fun ~from status -> profiler.CicUtil.profile (alias_diff ~from) status let set_proof_aliases status aliases = @@ -150,13 +150,17 @@ let save_object_to_disk status uri obj = [bodyuri, xmlbodypath] | _-> assert false) +let typecheck_obj = + let profiler = CicUtil.profile "add_obj.typecheck_obj" in + fun uri obj -> profiler.CicUtil.profile (CicTypeChecker.typecheck_obj uri) obj + let add_obj uri obj status = let dbd = MatitaDb.instance () in let suri = UriManager.string_of_uri uri in if CicEnvironment.in_library uri then command_error (sprintf "%s already defined" suri) else begin - CicTypeChecker.typecheck_obj uri obj; (* 1 *) + typecheck_obj uri obj; (* 1 *) try MetadataDb.index_obj ~dbd ~uri; (* 2 must be in the env *) try