src/Pure/General/file.scala

--- a/src/Pure/General/file.scala	Fri Jul 27 14:15:04 2012 +0200
+++ b/src/Pure/General/file.scala	Fri Jul 27 14:22:32 2012 +0200
@@ -35,6 +35,19 @@
   def read(path: Path): String = read(path.file)
 
 
+  /* 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 */
 
   private def write_file(file: JFile, text: CharSequence, gzip: Boolean)