X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatitadep.ml;h=0186a245a44269bb1f0f7227ee9bd866566cf0e4;hb=db068aa35cc47bb881ec810bf3b904c3d7cc9379;hp=cf1519eae7511cb2fb6aceeb2127c19984192e24;hpb=df666eb58afe0b312a2c4d41683d7ae4828ee8bd;p=helm.git

diff --git a/matita/matitadep.ml b/matita/matitadep.ml
index cf1519eae..0186a245a 100644
--- a/matita/matitadep.ml
+++ b/matita/matitadep.ml
@@ -37,23 +37,24 @@ let main () =
   let baseuri_of_inv = Hashtbl.create 13 in
   let dot_file = ref "" in
   (* helpers *)
-  let include_paths = 
-    Helm_registry.get_list Helm_registry.string "matita.includes" 
-  in
+  let include_paths = ref [] in
   let baseuri_of_script s = 
      try Hashtbl.find baseuri_of s 
      with Not_found -> 
-       let _,b,_,_ = Librarian.baseuri_of_script ~include_paths s in
+       let _,b,_,_ = 
+         Librarian.baseuri_of_script ~include_paths:!include_paths s 
+       in
        Hashtbl.add baseuri_of s b; 
        Hashtbl.add baseuri_of_inv b s; 
        b
   in
-  let script_of_baseuri b =
-    try Hashtbl.find baseuri_of_inv b
+  let script_of_baseuri ma b =
+    try Some (Hashtbl.find baseuri_of_inv b)
     with Not_found -> 
-     assert false 
-    (* should be called only after baseuri_of_script is
-     * called on every file *)
+      HLog.error ("Skipping dependency of '"^ma^"' over '"^b^"'");
+      HLog.error ("Plase include the file defining such baseuri, or fix");
+      HLog.error ("possibly incorrect verbatim URIs in the .ma file.");
+      None
   in
   let buri alias = U.buri_of_uri (U.uri_of_string alias) in
   let resolve alias current_buri =
@@ -74,6 +75,11 @@ let main () =
          exit 1
       | [x] -> 
          Sys.chdir (Filename.dirname x);
+         let opts = Librarian.load_root_file "root" in
+         include_paths := 
+           (try Str.split (Str.regexp " ") (List.assoc "include_paths" opts)
+           with Not_found -> []) @ 
+           (Helm_registry.get_list Helm_registry.string "matita.includes");
          HExtlib.find ~test:(fun x -> Filename.check_suffix x ".ma") "."
       | _ ->
          let roots = List.map (HExtlib.chop_prefix (Sys.getcwd()^"/")) roots in
@@ -100,8 +106,12 @@ let main () =
               let dep = resolve uri ma_baseuri in
               (match dep with 
               | None -> ()
-              | Some u -> Hashtbl.add include_deps ma_file (script_of_baseuri u))
+              | Some u -> 
+                  match script_of_baseuri ma_file u with
+                  | Some d -> Hashtbl.add include_deps ma_file d
+                  | None -> ())                
          | DependenciesParser.IncludeDep path -> 
+                ignore (baseuri_of_script path);
                 Hashtbl.add include_deps ma_file path)
        dependencies)
    ma_files;