- added support for "-nodb" flag (still missing support for matitaclean which relies...

[helm.git] / helm / matita / matitadep.ml

diff --git a/helm/matita/matitadep.ml b/helm/matita/matitadep.ml
index 40f91235a5a9e9ac82ae6d7e9c66f5253034a8f4..3eb83af00964690ebf276127c9fa44f3e1a412c3 100644 (file)
--- a/helm/matita/matitadep.ml
+++ b/helm/matita/matitadep.ml
@@ -23,18 +23,6 @@
  * http://helm.cs.unibo.it/
  *)
 
-let paths_to_search_in = ref [];;
-
-let add_l l = fun s -> l := s :: !l ;;
-
-let arg_spec = [
-  "-I", Arg.String (add_l paths_to_search_in), 
-    "<path> Adds path to the list of searched paths for the include command";
-]
-let usage =
-  Printf.sprintf "MatitaDep v%s\nUsage: matitadep [options] file...\nOptions:"
-    BuildTimeConf.version
-
 module GA = GrafiteAst 
 module U = UriManager
 
@@ -58,7 +46,7 @@ let find path =
         close_in (open_in (p ^ "/" ^ path)); p ^ "/" ^ path
       with Sys_error _ -> aux tl
   in
-  let paths = !paths_to_search_in in
+  let paths = Helm_registry.get_list Helm_registry.string "matita.includes" in
   try
     aux paths
   with Sys_error _ as exc ->
@@ -68,9 +56,8 @@ let find path =
 ;;
 
 let main () =
-  MatitaInit.load_config_only ();
-  let files = ref [] in
-  Arg.parse arg_spec (add_l files) usage;
+  MatitaInit.load_configuration_file ();
+  MatitaInit.parse_cmdline ();
   List.iter
    (fun file -> 
     let ic = open_in file in
@@ -94,7 +81,7 @@ let main () =
             MatitaLog.warn 
               ("Unable to find " ^ path ^ " that is included in " ^ file))
     dependencies)
-  !files;
+  (Helm_registry.get_list Helm_registry.string "matita.args");
   Hashtbl.iter 
     (fun file alias -> 
       let dep = resolve alias (Hashtbl.find baseuri_of file) in
@@ -112,7 +99,7 @@ let main () =
     let moo = MatitaMisc.obj_file_of_script file in
      Printf.printf "%s: %s\n" moo (String.concat " " deps);
      Printf.printf "%s: %s\n" (Pcre.replace ~pat:"ma$" ~templ:"mo" file) moo)
-  !files
+   (Helm_registry.get_list Helm_registry.string "matita.args")
 ;;
   
 let _ =