X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatitadep.ml;h=cfbc3783cbae5e624e842867e038a2ee576b88e0;hb=1776f357e1a69fa1133956660b65d7bafdfe5c25;hp=1ae74eafed52470b475f0dc6323712eb44b1fb17;hpb=4455a7194290db6bbe79c8bb52882d00997aa494;p=helm.git

diff --git a/matita/matitadep.ml b/matita/matitadep.ml
index 1ae74eafe..cfbc3783c 100644
--- a/matita/matitadep.ml
+++ b/matita/matitadep.ml
@@ -31,12 +31,12 @@ module U = UriManager
 let obj_file_of_baseuri writable baseuri = 
   try 
     LibraryMisc.obj_file_of_baseuri 
-     ~must_exist:true ~baseuri ~writable
+     ~must_exist:true ~baseuri ~writable 
   with 
   | Http_getter_types.Unresolvable_URI _ 
   | Http_getter_types.Key_not_found _ ->  
     LibraryMisc.obj_file_of_baseuri 
-     ~must_exist:false ~baseuri ~writable:true
+     ~must_exist:false ~baseuri ~writable:true 
 ;;
 
 let main () =
@@ -50,13 +50,12 @@ let main () =
   let resolve alias current_buri =
     let buri = buri alias in
     if buri <> current_buri then Some buri else None in
-  MatitaInit.fill_registry ();
   let dot_file = ref "" in
   MatitaInit.add_cmdline_spec 
     ["-dot", Arg.Set_string dot_file,
       "<file> Save dependency graph in dot format to the given file"];
-  MatitaInit.parse_cmdline ();
-  MatitaInit.load_configuration_file ();
+  MatitaInit.parse_cmdline_and_configuration_file ();
+  MatitaInit.initialize_environment ();
   let include_paths =
    Helm_registry.get_list Helm_registry.string "matita.includes" in
   let args = Helm_registry.get_list Helm_registry.string "matita.args" in
@@ -66,6 +65,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 +90,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;
@@ -107,11 +112,6 @@ let main () =
         prerr_endline ("File "^ file^" has no baseuri. Use set baseuri");
         exit 1)
   uri_deps;
-  if !dot_file <> "" then (* generate dependency graph if required *)
-    begin
-      let oc = open_out !dot_file in
-      let fmt = Format.formatter_of_out_channel oc in 
-      GraphvizPp.Dot.header (* ~graph_attrs:["rankdir","LR"] *) fmt;
       let gcp x y = 
       (* explode and implode from the OCaml Expert FAQ. *)
         let explode s =
@@ -135,6 +135,11 @@ let main () =
       let max_path = List.hd ma_files in 
       let max_path = List.fold_left gcp max_path ma_files in
       let short x = Pcre.replace ~pat:("^"^max_path) x in
+  if !dot_file <> "" then (* generate dependency graph if required *)
+    begin
+      let oc = open_out !dot_file in
+      let fmt = Format.formatter_of_out_channel oc in 
+      GraphvizPp.Dot.header (* ~graph_attrs:["rankdir","LR"] *) fmt;
       List.iter
        (fun ma_file -> 
         let deps = Hashtbl.find_all include_deps_dot ma_file in
@@ -162,10 +167,11 @@ let main () =
       let deps = ma_file :: deps in
       let baseuri = Hashtbl.find baseuri_of ma_file in
       let moo = obj_file_of_baseuri true baseuri in
-      Printf.printf "%s: %s\n%s: %s\n%s: %s\n" 
+      Printf.printf "%s: %s\n%s: %s\n%s: %s\n%s: %s\n" 
         moo (String.concat " " deps)
         (Filename.basename(Pcre.replace ~pat:"ma$" ~templ:"mo" ma_file)) moo
         (Pcre.replace ~pat:"ma$" ~templ:"mo" ma_file) moo
+        (Pcre.replace ~pat:"ma$" ~templ:"mo" (short ma_file)) moo
      with Not_found -> 
        prerr_endline ("File "^ma_file^" has no baseuri. Use set baseuri");
        exit 1)