]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/matitadep.ml
- transcript: we have now two styles of mma's from grafite:
[helm.git] / helm / software / matita / matitadep.ml
index 514147bd17cb502a1421b966e76eb7731456b382..af811b140741372f7e44b15c98d4764eec3e37fa 100644 (file)
@@ -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 <name>", Arg.String set_theory_file,
+        "generate a theory file <name>.ma (it includes all other files)"
     ];
   MatitaInit.parse_cmdline_and_configuration_file ();
   MatitaInit.initialize_environment ();