clarified signature;
authorwenzelm
Thu, 20 Dec 2018 22:56:36 +0100
changeset 69499 681760f50723
parent 69498 59ada9f63cc5
child 69500 b05c0bb47f6d
clarified signature;
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