# HG changeset patch
# User wenzelm
# Date 1545342996 -3600
# Node ID 681760f50723585d8cf6d59cc8f03c96ae68c846
# Parent  59ada9f63cc5bffccb509d28062f13a9e23ccbde
clarified signature;

diff -r 59ada9f63cc5 -r 681760f50723 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Thu Dec 20 16:34:23 2018 +0100
+++ b/src/Pure/General/file.scala	Thu Dec 20 22:56:36 2018 +0100
@@ -211,13 +211,21 @@
 
   /* read lines */
 
+  def read_line(reader: BufferedReader): Option[String] =
+  {
+    val line =
+      try { reader.readLine}
+      catch { case _: IOException => null }
+    if (line == null) None else Some(line)
+  }
+
   def read_lines(reader: BufferedReader, progress: String => Unit): List[String] =
   {
     val result = new mutable.ListBuffer[String]
-    var line: String = null
-    while ({ line = try { reader.readLine} catch { case _: IOException => null }; line != null }) {
-      progress(line)
-      result += line
+    var line: Option[String] = None
+    while ({ line = read_line(reader); line.isDefined }) {
+      progress(line.get)
+      result += line.get
     }
     reader.close
     result.toList