From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 22 Dec 2006 08:54:57 +0000 (+0000)
Subject: Speeedup! (by caching)
X-Git-Tag: 0.4.95@7852~713
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=df70518efb295cdce60a3df8098ac0a6eef2d9cf;p=helm.git

Speeedup! (by caching)
The costing operation is baseuri_of_file that parses the whole maybe big file to extract the first command line.
---

diff --git a/matita/matitadep.ml b/matita/matitadep.ml
index 7f75a057b..f62a6067f 100644
--- a/matita/matitadep.ml
+++ b/matita/matitadep.ml
@@ -66,6 +66,13 @@ let main () =
       exit 1
     end;
   let ma_files = args in
+  let bof = Hashtbl.create 10 in
+  let baseuri_of_script s = 
+     try Hashtbl.find bof s 
+     with Not_found -> 
+       let b,_ = DependenciesParser.baseuri_of_script ~include_paths s in
+       Hashtbl.add bof s b; b
+  in
   List.iter
    (fun ma_file -> 
     let ic = open_in ma_file in
@@ -84,8 +91,7 @@ let main () =
           Hashtbl.add baseuri_of_inv uri ma_file
        | DependenciesParser.IncludeDep path -> 
           try 
-            let baseuri,_ =
-              DependenciesParser.baseuri_of_script ~include_paths path in
+            let baseuri = baseuri_of_script path in
             if not (Http_getter_storage.is_legacy baseuri) then
               (let moo_file = obj_file_of_baseuri false baseuri in
               Hashtbl.add include_deps ma_file moo_file;