# HG changeset patch
# User wenzelm
# Date 1261945854 -3600
# Node ID b91953f894a844bc2e05a156372e8d0607e314f3
# Parent  9316b8f56d83117f4d0277cd8c20811dd6bd9a37
removed unused read_file;

diff -r 9316b8f56d83 -r b91953f894a8 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Thu Dec 24 17:30:55 2009 +0000
+++ b/src/Pure/System/isabelle_system.scala	Sun Dec 27 21:30:54 2009 +0100
@@ -45,22 +45,6 @@
     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
-    }
-    reader.close
-    buf.toString
-  }
 }