X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatitadep.ml;h=fe7cab92075ee99c3dd74bfe57d71934e4cbbb99;hb=5044ed858486dc12ad7cd1c2f2f22c62d9c8708d;hp=42034c1a880a785c38402757bceca72abc41c862;hpb=3c8a3783837bf7773437b12a089b8edf93879b5d;p=helm.git

diff --git a/matita/matitadep.ml b/matita/matitadep.ml
index 42034c1a8..fe7cab920 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,10 +75,16 @@ 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") "."
       | _ ->
-         prerr_endline ("Too many roots: " ^ String.concat ", " roots);
-         prerr_endline ("Enter one of these directories and retry");
+         let roots = List.map (HExtlib.chop_prefix (Sys.getcwd()^"/")) roots in
+         prerr_endline ("Too many roots found:\n\t" ^ String.concat "\n\t" roots);
+         prerr_endline ("\nEnter one of these directories and retry");
          exit 1
   in
   let ma_files = args in
@@ -99,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;
@@ -158,6 +169,8 @@ let main () =
           acc d)
       [] deps
   in
-  Librarian.write_deps_file (Sys.getcwd()) (deps@List.map (fun x -> x,[]) extern)
+  Librarian.write_deps_file (Sys.getcwd()) 
+   (deps@HExtlib.list_uniq (List.sort Pervasives.compare (List.map (fun x ->
+           x,[]) extern)))
 ;;