updating the structures for sorts

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

diff --git a/helm/software/matita/matitac.ml b/helm/software/matita/matitac.ml
index 5d0ed9a3512528c8a45886606efd1131dd45677e..83ab74439129e005717d987083b8bdbbb9b2a908 100644 (file)
--- a/helm/software/matita/matitac.ml
+++ b/helm/software/matita/matitac.ml
@@ -42,12 +42,15 @@ 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);
-    | [hd] -> 
-      let root, buri, file, target =
-        Librarian.baseuri_of_script ~include_paths:[] hd 
-      in
-      [target], root
-    | _ -> prerr_endline "Only one target (or none) can be specified.";exit 1
+    | hds -> 
+      let roots_and_targets = 
+       List.map (fun (root, buri, file, target) -> root,target)
+        (List.map (Librarian.baseuri_of_script ~include_paths:[]) hds) in
+      let roots,targets = List.split roots_and_targets in
+      let root = List.hd roots in
+      if (List.exists (fun root' -> root' <> root) roots) then
+       (prerr_endline "Only targets in the same root can be specified.";exit 1);
+      targets, root
   in
   (* must be called after init since args are set by cmdline parsing *)
   let system_mode =  Helm_registry.get_bool "matita.system" in
@@ -55,17 +58,18 @@ let main_compiler () =
   (* here we go *)
   if not (Helm_registry.get_bool "matita.verbose") then MatitaMisc.shutup ();
   if MatitacLib.Make.make root target then 
-    HLog.message "Compilation successful"
+    (HLog.message "Compilation successful"; 0)
   else
-    HLog.message "Compilation failed"
+    (HLog.message "Compilation failed"; 1)
 ;;
 
 let main () =
+  Sys.catch_break true;
   let bin = Filename.basename Sys.argv.(0) in
   if      Pcre.pmatch ~pat:"^matitadep"    bin then Matitadep.main ()
   else if Pcre.pmatch ~pat:"^matitaclean"  bin then Matitaclean.main ()
   else if Pcre.pmatch ~pat:"^matitawiki"   bin then MatitaWiki.main ()
-  else main_compiler ()
+  else exit (main_compiler ())
 ;;
 
 let _ = main ()