X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=9707149d568cd52bb87de6846f782bebce038322;hb=dc861d214cb992a898f81752614201b8074eef12;hp=a744ba925ee73bdd09ae0b5ba9de0c7db2328af0;hpb=0a744f0790c6483f0e962e7392b1f588ec10895d;p=helm.git

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index a744ba925..9707149d5 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -501,12 +501,12 @@ let disambiguate_command status = function
       let status,obj = disambiguate_obj status obj in
        status, GrafiteAst.Obj (loc,obj)
 
-let try_open_in paths path =
+let try_open_in ~f paths path =
   let rec aux = function
-  | [] -> open_in path
+  | [] -> f path
   | p :: tl ->
       try
-        open_in (p ^ "/" ^ path)
+        f (p ^ "/" ^ path)
       with Sys_error _ -> aux tl
   in
   try
@@ -531,14 +531,14 @@ let eval_command opts status cmd =
         (GrafiteAstPp.pp_command cmd ^ "\n") :: status.moo_content_rev}
   | GrafiteAst.Include (loc, path) ->
      let path = MatitaMisc.obj_file_of_script 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
+     (try
+       let ic = try_open_in ~f:open_in opts.include_paths path in
+       let stream = Stream.of_channel ic in
+       let status = ref status in
+       !eval_from_stream_ref status stream (fun _ _ -> ());
+       close_in ic;
+       !status
+     with Sys_error _ -> raise (UnableToInclude path))
   | GrafiteAst.Set (loc, name, value) -> 
       let value = 
         if name = "baseuri" then