Use of standard OCaml syntax

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

diff --git a/matita/matita/matitac.ml b/matita/matita/matitac.ml
index a93d694dcc240a2e17646cc14c3194c0e58c5344..c2291d5754c60cc5cec2619a107a74acb5d98448 100644 (file)
--- a/matita/matita/matitac.ml
+++ b/matita/matita/matitac.ml
@@ -44,13 +44,20 @@ let main_compiler () =
          prerr_endline ("Too many roots found:\n\t" ^ String.concat "\n\t" roots);
          prerr_endline ("\nEnter one of these directories and retry");
          exit 1);
-    | _ -> targets
+    | _ ->
+      let map targets file =
+          if HExtlib.is_dir file then
+             let files = HExtlib.find ~test:(fun path -> Filename.check_suffix path ".ma") file in
+             files @ targets
+          else file :: targets
+      in
+      List.fold_left map [] (List.rev targets)
   in
   (* must be called after init since args are set by cmdline parsing *)
   let system_mode =  Helm_registry.get_bool "matita.system" in
   if system_mode then HLog.message "Compiling in system space";
   (* here we go *)
-  if not (Helm_registry.get_bool "matita.verbose") then MatitaMisc.shutup ();
+  if not (Helm_registry.get_bool "matita.verbose") then MatitaMiscCli.shutup ();
   if List.fold_left
    (fun b t ->
      (try
@@ -67,9 +74,7 @@ let main_compiler () =
 
 let main () =
   Sys.catch_break true;
-  let bin = Filename.basename Sys.argv.(0) in
-  if Pcre.pmatch ~pat:"^matitaclean"  bin then Matitaclean.main ()
-  else exit (main_compiler ())
+  exit (main_compiler ())
 ;;
 
 let _ = main ()