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

diff --git a/matita/matitadep.ml b/matita/matitadep.ml
index 2fc72ad8a..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 =
@@ -66,10 +67,7 @@ let main () =
     "<file> Save dependency graph in dot format to the given file";];
   MatitaInit.parse_cmdline_and_configuration_file ();
   MatitaInit.initialize_environment ();
-  MatitamakeLib.initialize ();
-  let args = Helm_registry.get_list Helm_registry.string "matita.args" in
   let args = 
-    if args = [] then
       let roots = Librarian.find_roots_in_dir (Sys.getcwd ()) in
       match roots with
       | [] -> 
@@ -77,18 +75,22 @@ 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
-    else
-      args
   in
   let ma_files = args in
   (* here we go *)
   (* fills:
-              Hashtbl.add include_deps     ma_file moo_file
+              Hashtbl.add include_deps     ma_file ma_file
               Hashtbl.add include_deps_dot ma_file baseuri
   *)
   List.iter (fun ma_file -> ignore (baseuri_of_script ma_file)) ma_files;
@@ -104,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;
@@ -134,24 +140,37 @@ let main () =
       close_out oc
     end;
   (* generate regular depend output *)
-  let oc = open_out "depends" in
-  List.iter 
-   (fun ma_file -> 
+  let fix_name f =
+    let f = 
+      if Pcre.pmatch ~pat:"^\\./" f then
+        String.sub f 2 (String.length f - 2)
+      else 
+        f
+    in 
+      HExtlib.normalize_path f
+  in
+  let deps =
+    List.fold_left
+     (fun acc ma_file -> 
       let deps = Hashtbl.find_all include_deps ma_file in
       let deps = List.fast_sort Pervasives.compare deps in
       let deps = HExtlib.list_uniq deps in
-      let deps = ma_file :: deps in
-      let deps = 
-        List.map (fun f ->
-                let f = 
-                  if Pcre.pmatch ~pat:"^\\./" f then
-                    String.sub f 2 (String.length f - 2)
-                  else 
-                    f
-                in HExtlib.normalize_path f) deps 
-      in
-      output_string oc (String.concat " " deps ^ "\n"))
-   ma_files;
-  close_out oc;
-  HLog.message ("Generated " ^ Sys.getcwd () ^ "/depends")
+      let deps = List.map fix_name deps in
+      (fix_name ma_file, deps) :: acc)
+     [] ma_files
+  in
+  let extern = 
+    List.fold_left
+      (fun acc (_,d) -> 
+        List.fold_left 
+          (fun a x -> 
+             if List.exists (fun (t,_) -> x=t) deps then a 
+             else x::a) 
+          acc d)
+      [] deps
+  in
+  Librarian.write_deps_file (Sys.getcwd()) 
+   (deps@HExtlib.list_uniq (List.sort Pervasives.compare (List.map (fun x ->
+           x,[]) extern)))
+;;