src/Pure/Thy/thy_header.scala
changeset 48882 61dc7d5d150a
parent 48864 3ee314ae1e0a
child 50128 599c935aac82
     1.1 --- a/src/Pure/Thy/thy_header.scala	Wed Aug 22 12:47:49 2012 +0200
     1.2 +++ b/src/Pure/Thy/thy_header.scala	Wed Aug 22 15:53:17 2012 +0200
     1.3 @@ -106,13 +106,6 @@
     1.4    def read(source: CharSequence): Thy_Header =
     1.5      read(new CharSequenceReader(source))
     1.6  
     1.7 -  def read(file: JFile): Thy_Header =
     1.8 -  {
     1.9 -    val reader = Scan.byte_reader(file)
    1.10 -    try { read(reader).map(Standard_System.decode_permissive_utf8) }
    1.11 -    finally { reader.close }
    1.12 -  }
    1.13 -
    1.14  
    1.15    /* keywords */
    1.16