X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fmatitadep.ml;h=050fa220e87d84fd3bf2c54329d2d81c21b02090;hb=5fa31e43ffe25aa7b1539653b137968b5cf9899a;hp=c0d784637b07a540f0059452599c3ce1a4bf0728;hpb=662f191b09d1b9e3d13e4f9ee5c174c1ac08fadb;p=helm.git diff --git a/helm/software/matita/matitadep.ml b/helm/software/matita/matitadep.ml index c0d784637..050fa220e 100644 --- a/helm/software/matita/matitadep.ml +++ b/helm/software/matita/matitadep.ml @@ -40,7 +40,8 @@ let fix_name f = else f in HExtlib.normalize_path f - + +(* FG: old function left for reference *) let exclude excluded_files files = let map file = not (List.mem (fix_name file) excluded_files) in List.filter map files @@ -48,7 +49,6 @@ let exclude excluded_files files = let main () = (* let _ = print_times "inizio" in *) let include_paths = ref [] in - let excluded_files = ref [] in let use_stdout = ref false in (* all are maps from "file" to "something" *) let include_deps = Hashtbl.create 13 in @@ -57,7 +57,6 @@ let main () = let dot_name = "depends" in let dot_file = ref "" in let set_dot_file () = dot_file := dot_name^".dot" in - let set_excluded_file name = excluded_files := name :: !excluded_files in (* helpers *) let rec baseuri_of_script s = try Hashtbl.find baseuri_of s @@ -91,8 +90,6 @@ let main () = MatitaInit.add_cmdline_spec ["-dot", Arg.Unit set_dot_file, "Save dependency graph in dot format and generate a png"; - "-exclude", Arg.String set_excluded_file, - "Exclude a file from the dependences"; "-stdout", Arg.Set use_stdout, "Print dependences on stdout" ]; @@ -127,7 +124,6 @@ let main () = prerr_endline ("\nEnter one of these directories and retry"); exit 1 in - let args = exclude !excluded_files args in let ma_files = args in (* here we go *) (* fills: @@ -150,22 +146,30 @@ let main () = try DependenciesParser.deps_of_file ma_file with Sys_error _ -> [] in + let handle_uri uri = + if not (Http_getter_storage.is_legacy uri) then + let dep = resolve uri ma_baseuri in + match dep with + | None -> () + | Some u -> + match script_of_baseuri ma_file u with + | Some d -> Hashtbl.add include_deps ma_file d + | None -> () + in + let handle_script path = + ignore (baseuri_of_script path); + Hashtbl.add include_deps ma_file path + in List.iter (function - | DependenciesParser.UriDep uri -> + | DependenciesParser.UriDep uri -> let uri = UriManager.string_of_uri uri in - if not (Http_getter_storage.is_legacy uri) then - let dep = resolve uri ma_baseuri in - (match dep with - | None -> () - | Some u -> - match script_of_baseuri ma_file u with - | Some d -> Hashtbl.add include_deps ma_file d - | None -> ()) - | DependenciesParser.InlineDep path - | DependenciesParser.IncludeDep path -> - ignore (baseuri_of_script path); - Hashtbl.add include_deps ma_file path) + handle_uri uri + | DependenciesParser.InlineDep path -> + if Librarian.is_uri path + then handle_uri path else handle_script path + | DependenciesParser.IncludeDep path -> + handle_script path) dependencies) ma_files; (* generate regular depend output *) @@ -214,5 +218,3 @@ let main () = HLog.message ("Type 'eog "^dot_name^".png' to view the graph"); end; (* let _ = print_times "fine" in () *) - -