X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fmatitadep.ml;h=af811b140741372f7e44b15c98d4764eec3e37fa;hb=eadeb433386822aac6862c76ba73957c07a99098;hp=514147bd17cb502a1421b966e76eb7731456b382;hpb=93cc2a2254a2620000377dfc99a7aaedf2b8ec63;p=helm.git diff --git a/helm/software/matita/matitadep.ml b/helm/software/matita/matitadep.ml index 514147bd1..af811b140 100644 --- a/helm/software/matita/matitadep.ml +++ b/helm/software/matita/matitadep.ml @@ -49,6 +49,7 @@ let exclude excluded_files files = List.filter map files let generate_theory theory_file deps = + if theory_file = "" then deps else let map (files, deps) (t, d) = if t = theory_file then files, deps else S.add t files, List.fold_left (fun deps dep -> S.add dep deps) deps d @@ -59,16 +60,18 @@ let generate_theory theory_file deps = let fileset, depset = List.fold_left map (S.empty, S.empty) deps in let top_depset = S.diff fileset depset in let och = open_out theory_file in - MatitaMisc.out_preamble och; - S.iter (out_include och) top_depset; - close_out och; - (theory_file, S.elements top_depset) :: deps + begin + MatitaMisc.out_preamble och; + S.iter (out_include och) top_depset; + close_out och; + (theory_file, S.elements top_depset) :: deps + end let main () = (* let _ = print_times "inizio" in *) let include_paths = ref [] in let use_stdout = ref false in - let theory_file = ref "theory.ma" in + let theory_file = ref "" in (* all are maps from "file" to "something" *) let include_deps = Hashtbl.create 13 in let baseuri_of = Hashtbl.create 13 in @@ -112,8 +115,8 @@ let main () = "Save dependency graph in dot format and generate a png"; "-stdout", Arg.Set use_stdout, "Print dependences on stdout"; - "-theory", Arg.String set_theory_file, - "Set the name of the theory file (it includes all other files)" + "-theory ", Arg.String set_theory_file, + "generate a theory file .ma (it includes all other files)" ]; MatitaInit.parse_cmdline_and_configuration_file (); MatitaInit.initialize_environment ();