avoid Source.fromFile, which does not necessarily close its input;
authorwenzelm
Tue, 17 Jul 2012 16:56:29 +0200
changeset 48278 2b737f639ad4
parent 48277 f14e564fca1a
child 48279 ddf866029eb2
avoid Source.fromFile, which does not necessarily close its input;
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
   }