matitamake is integrated with matita

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

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index c3a8be67d3d6c1a3f2e90b246c18f252925c0907..cf83195dc8c97cbf58b93edd5d1d228876b3f592 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -3,6 +3,7 @@ open Printf
 open MatitaTypes
 
 exception Drop;;
+exception UnableToInclude of string;;
 
 let debug = false ;;
 let debug_print = if debug then prerr_endline else ignore ;;
@@ -458,6 +459,7 @@ let try_open_in paths path =
   with Sys_error _ as exc ->
     MatitaLog.error ("Unable to read " ^ path);
     MatitaLog.error ("opts.include_paths was " ^ String.concat ":" paths);
+    MatitaLog.error ("current working directory is " ^ Unix.getcwd ());
     raise exc
 ;;
        
@@ -470,7 +472,11 @@ let eval_command opts status cmd =
         (TacticAstPp.pp_command cmd ^ "\n") :: status.moo_content_rev}
   | TacticAst.Include (loc, path) ->
      let path = MatitaMisc.obj_file_of_script path in
-     let stream = Stream.of_channel (try_open_in opts.include_paths path) in
+     let stream = 
+       try
+         Stream.of_channel (try_open_in opts.include_paths path) 
+       with Sys_error _ -> raise (UnableToInclude path)
+     in
      let status = ref status in
       !eval_from_stream_ref status stream (fun _ _ -> ());
       !status