# HG changeset patch
# User wenzelm
# Date 1261498423 -3600
# Node ID 610ec1e0c8485e2c437d8a9391d2823decce4890
# Parent  4c845a8f13574b8e4c64e8f964bb3a41665d18ff
added plain read_file;

diff -r 4c845a8f1357 -r 610ec1e0c848 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Tue Dec 22 17:13:18 2009 +0100
+++ b/src/Pure/System/isabelle_system.scala	Tue Dec 22 17:13:43 2009 +0100
@@ -8,7 +8,8 @@
 
 import java.util.regex.Pattern
 import java.util.Locale
-import java.io.{BufferedInputStream, FileInputStream, File, IOException}
+import java.io.{BufferedInputStream, FileInputStream, BufferedReader, InputStreamReader,
+  File, IOException}
 import java.awt.{GraphicsEnvironment, Font}
 
 import scala.io.Source
@@ -43,6 +44,21 @@
     val rc = proc.waitFor
     (output, rc)
   }
+
+
+  /* platform files */
+
+  def read_file(file: File): String =
+  {
+    val buf = new StringBuilder(file.length.toInt)
+    val reader = new BufferedReader(new InputStreamReader(new FileInputStream(file), charset))
+    var c = reader.read
+    while (c != -1) {
+      buf.append(c.toChar)
+      c = reader.read
+    }
+    buf.toString
+  }
 }