fixed error message

[helm.git] / matita / matitac.ml

diff --git a/matita/matitac.ml b/matita/matitac.ml
index 199b041576550d2a1b952dd96e5ef2112087238d..c31c22874e2038dccd675f1c5cfd2c394a4d6841 100644 (file)
--- a/matita/matitac.ml
+++ b/matita/matitac.ml
@@ -89,29 +89,34 @@ let main_compiler () =
   MatitaInit.initialize_all ();
   (* targets and deps *)
   let targets = Helm_registry.get_list Helm_registry.string "matita.args" in
-  let deps, target = 
+  let target, root = 
     match targets with
     | [] ->
       (match Librarian.find_roots_in_dir (Sys.getcwd ()) with
-      | [x] -> 
-         Make.load_deps_file (Filename.dirname x ^ "/depends"), []
+      | [x] -> [], x
       | [] -> 
-         HLog.error "No targets and no root found"; exit 1
+         prerr_endline "No targets and no root found"; exit 1
       | roots -> 
-         HLog.error ("Too many roots found, move into one and retry: "^
-           String.concat ", " roots);exit 1);
+         let roots = List.map (HExtlib.chop_prefix (Sys.getcwd()^"/")) roots in
+         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 hd in
-      HLog.debug ("Compiling target '" ^ target ^ "' with base uri '"^buri^"'");
-      Make.load_deps_file (root ^ "/depends"), [target]
-    | _ -> HLog.error "Only one target (or none) can be specified.";exit 1
+      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
   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";
-  if not (Helm_registry.get_bool "matita.verbose") then MatitaMisc.shutup ();
   (* here we go *)
-  MatitacLib.Make.make deps target
+  if not (Helm_registry.get_bool "matita.verbose") then MatitaMisc.shutup ();
+  if MatitacLib.Make.make root target then 
+    HLog.message "Compilation successful"
+  else
+    HLog.message "Compilation failed"
 ;;
 
 let main () =