# HG changeset patch
# User wenzelm
# Date 1451402614 -3600
# Node ID 364007370bb75896ef51605a5ab807f76a0dd3a5
# Parent  0a5dd617a88c64d8bfb6c083162ee74b96a3daa8
tuned;

diff -r 0a5dd617a88c -r 364007370bb7 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Tue Dec 29 15:05:08 2015 +0100
+++ b/src/Pure/General/file.scala	Tue Dec 29 16:23:34 2015 +0100
@@ -164,19 +164,6 @@
   }
 
 
-  /* try_read */
-
-  def try_read(paths: Seq[Path]): String =
-  {
-    val buf = new StringBuilder
-    for (path <- paths if path.is_file) {
-      buf.append(read(path))
-      buf.append('\n')
-    }
-    buf.toString
-  }
-
-
   /* write */
 
   def write_file(file: JFile, text: Iterable[CharSequence],
diff -r 0a5dd617a88c -r 364007370bb7 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Tue Dec 29 15:05:08 2015 +0100
+++ b/src/Pure/General/symbol.scala	Tue Dec 29 16:23:34 2015 +0100
@@ -285,7 +285,12 @@
   /** symbol interpretation **/
 
   private lazy val symbols =
-    new Interpretation(File.try_read(Path.split(Isabelle_System.getenv("ISABELLE_SYMBOLS"))))
+  {
+    val contents =
+      for (path <- Path.split(Isabelle_System.getenv("ISABELLE_SYMBOLS")) if path.is_file)
+        yield (File.read(path))
+    new Interpretation(cat_lines(contents))
+  }
 
   private class Interpretation(symbols_spec: String)
   {