From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 19 Jul 2005 17:24:41 +0000 (+0000)
Subject: fixed file descriptor leak
X-Git-Tag: V_0_7_2~160
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=564dea6c0486749e3ad9b324d5077298f65c0d5e;hp=ea2a86fd71f541b2b0c5c2ba217be75fd2cb5fe5;p=helm.git

fixed file descriptor leak
---

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