clarified: more uniform;

--- a/src/Pure/General/file.scala	Tue Nov 24 16:49:42 2020 +0100
+++ b/src/Pure/General/file.scala	Wed Nov 25 12:34:08 2020 +0100
@@ -222,7 +222,7 @@
     val line =
       try { reader.readLine}
       catch { case _: IOException => null }
-    Option(line)
+    Option(line).map(Library.trim_line)
   }
 
   def read_lines(reader: BufferedReader, progress: String => Unit): List[String] =