From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 23 Sep 2005 16:16:09 +0000 (+0000)
Subject: CicUtil.profile ==> HExtlib.profile
X-Git-Tag: LAST_BEFORE_NEW~21
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2eeeed0dca0fd4fde2c0ec2b98db40d327e7e158;p=helm.git

CicUtil.profile ==> HExtlib.profile
---

diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml
index cd4d42420..22819536f 100644
--- a/helm/matita/matitaDisambiguator.ml
+++ b/helm/matita/matitaDisambiguator.ml
@@ -135,10 +135,10 @@ type disambiguator_thing =
  }
 
 let disambiguate_thing =
- let profiler = CicUtil.profile "disambiguate_thing" in
+ let profiler = HExtlib.profile "disambiguate_thing" in
   { do_it =
      fun ~aliases ~universe ~f ~drop_aliases ~drop_aliases_and_clear_diff thing
-     -> profiler.CicUtil.profile
+     -> profiler.HExtlib.profile
          (disambiguate_thing ~aliases ~universe ~f ~drop_aliases
            ~drop_aliases_and_clear_diff) thing
   }
diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 79c6a4dde..9a194b5ba 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -696,7 +696,7 @@ let make_absolute paths path =
    with Unix.Unix_error _ as exc -> raise (UnableToInclude path)
 ;;
        
-let profiler_include = CicUtil.profile "include"
+let profiler_include = HExtlib.profile "include"
 
 let eval_command opts status cmd =
   let status,cmd = disambiguate_command status cmd in
@@ -716,7 +716,7 @@ let eval_command opts status cmd =
         raise (IncludedFileNotCompiled moopath) in
      let stream = Ulexing.from_utf8_channel ic in
      let status = ref status in
-      profiler_include.CicUtil.profile
+      profiler_include.HExtlib.profile
        (!eval_from_stream_ref status stream) (fun _ _ -> ());
       close_in ic;
       !status
diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index 95dab0360..9a8cb10ee 100644
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -43,8 +43,8 @@ let alias_diff ~from status =
     status.aliases []
 
 let alias_diff =
- let profiler = CicUtil.profile "alias_diff (conteggiato anche in include)" in
- fun ~from status -> profiler.CicUtil.profile (alias_diff ~from) status
+ let profiler = HExtlib.profile "alias_diff (conteggiato anche in include)" in
+ fun ~from status -> profiler.HExtlib.profile (alias_diff ~from) status
 
 let set_proof_aliases status new_aliases =
  let aliases =
@@ -158,18 +158,13 @@ let save_object_to_disk status uri obj ugraph univlist =
      | _-> 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 profiler = HExtlib.profile "add_obj.typecheck_obj" in
+  fun uri obj -> profiler.HExtlib.profile (CicTypeChecker.typecheck_obj uri) obj
 
 let index_obj =
- let profiler = CicUtil.profile "add_obj.index_obj" in
+ let profiler = HExtlib.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 ugraph univlist ->
-   profiler.CicUtil.profile (save_object_to_disk status uri obj ugraph) univlist
+   profiler.HExtlib.profile (fun uri -> MetadataDb.index_obj ~dbd ~uri) uri
 
 let add_obj uri obj status =
   let dbd = MatitaDb.instance () in
@@ -201,8 +196,8 @@ let add_obj uri obj status =
   end
 
 let add_obj =
- let profiler = CicUtil.profile "add_obj" in
-  fun uri obj status -> profiler.CicUtil.profile (add_obj uri obj) status
+ let profiler = HExtlib.profile "add_obj" in
+  fun uri obj status -> profiler.HExtlib.profile (add_obj uri obj) status
    
 module OrderedUri =
 struct