tuned;
authorwenzelm
Tue, 29 Dec 2015 16:23:34 +0100
changeset 61959 364007370bb7
parent 61958 0a5dd617a88c
child 61960 20c1321378db
tuned;
src/Pure/General/file.scala
src/Pure/General/symbol.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],
--- 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)
   {