more permissive File.read_lines, which is relevant for Managed_Process join/kill;

--- a/src/Pure/General/file.scala	Sat Feb 23 11:27:45 2013 +0100
+++ b/src/Pure/General/file.scala	Sat Feb 23 12:28:18 2013 +0100
@@ -9,7 +9,7 @@
 
 import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream,
   InputStream, FileInputStream, BufferedInputStream, BufferedReader, InputStreamReader,
-  File => JFile}
+  File => JFile, IOException}
 import java.util.zip.{GZIPInputStream, GZIPOutputStream}
 
 import scala.collection.mutable
@@ -81,7 +81,7 @@
   {
     val result = new mutable.ListBuffer[String]
     var line: String = null
-    while ({ line = reader.readLine; line != null }) {
+    while ({ line = try { reader.readLine} catch { case _: IOException => null }; line != null }) {
       progress(line)
       result += line
     }