# HG changeset patch
# User wenzelm
# Date 1342536989 -7200
# Node ID 2b737f639ad43305385b1d0f5ce09ab62aed0841
# Parent  f14e564fca1aa58a7be67962094477f65d016113
avoid Source.fromFile, which does not necessarily close its input;

diff -r f14e564fca1a -r 2b737f639ad4 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Tue Jul 17 16:54:23 2012 +0200
+++ b/src/Pure/System/isabelle_system.scala	Tue Jul 17 16:56:29 2012 +0200
@@ -78,7 +78,7 @@
               if (rc != 0) error(output)
 
               val entries =
-                (for (entry <- Source.fromFile(dump).mkString split "\0" if entry != "") yield {
+                (for (entry <- Standard_System.read_file(dump) split "\0" if entry != "") yield {
                   val i = entry.indexOf('=')
                   if (i <= 0) (entry -> "")
                   else (entry.substring(0, i) -> entry.substring(i + 1))
@@ -132,8 +132,7 @@
     for {
       path <- paths
       file = platform_file(path) if file.isFile
-      c <- (Source.fromFile(file) ++ Iterator.single('\n'))
-    } buf.append(c)
+    } { buf.append(Standard_System.read_file(file)); buf.append('\n') }
     buf.toString
   }