]> matita.cs.unibo.it Git - helm.git/commitdiff
Profiling code removed.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 23 Sep 2005 14:14:05 +0000 (14:14 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 23 Sep 2005 14:14:05 +0000 (14:14 +0000)
helm/ocaml/metadata/metadataDb.ml

index 2fdfb49fd49a02056c502dd4b6463651462f1194..8d963bfc47cb75a8f0f880a530da3fc6e66da8c9 100644 (file)
@@ -142,27 +142,15 @@ let eventually_analyze dbd =
   
 (***** TENTATIVE HACK FOR THE DB SLOWDOWN - END *******)
 
-let profile = (CicUtil.profile "foo").CicUtil.profile
-let profile2 = (CicUtil.profile "foo2").CicUtil.profile
-let profile3 = (CicUtil.profile "foo3").CicUtil.profile
-
 let index_obj ~dbd ~uri = 
   if not (already_indexed uri) then begin
-let foo () =
     eventually_analyze dbd;
-in profile3 foo ();
-    let metadata =
-let foo () =
-MetadataExtractor.compute_obj uri in
-profile2 foo () in
+    let metadata = MetadataExtractor.compute_obj uri in
     let uri = UriManager.string_of_uri uri in
-    let columns =
-MetadataPp.columns_of_metadata metadata in
-let foo () =
+    let columns = MetadataPp.columns_of_metadata metadata in
     execute_insert dbd uri (columns :> columns);
     insert_const_no ~dbd metadata;
     insert_name ~dbd metadata
-in profile foo ()
   end