src/Pure/PIDE/resources.scala
changeset 56823 37be55461dbe
parent 56801 8dd9df88f647
child 56913 df4cd6e1fdfa
     1.1 --- a/src/Pure/PIDE/resources.scala	Fri May 02 12:27:40 2014 +0200
     1.2 +++ b/src/Pure/PIDE/resources.scala	Fri May 02 13:52:45 2014 +0200
     1.3 @@ -8,6 +8,7 @@
     1.4  
     1.5  
     1.6  import scala.annotation.tailrec
     1.7 +import scala.util.parsing.input.Reader
     1.8  
     1.9  import java.io.{File => JFile}
    1.10  
    1.11 @@ -40,14 +41,13 @@
    1.12    def append(dir: String, source_path: Path): String =
    1.13      (Path.explode(dir) + source_path).expand.implode
    1.14  
    1.15 -  def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A =
    1.16 +  def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
    1.17    {
    1.18      val path = Path.explode(name.node)
    1.19      if (!path.is_file) error("No such file: " + path.toString)
    1.20  
    1.21 -    val text = File.read(path)
    1.22 -    Symbol.decode_strict(text)
    1.23 -    f(text)
    1.24 +    val reader = Scan.byte_reader(path.file)
    1.25 +    try { f(reader) } finally { reader.close }
    1.26    }
    1.27  
    1.28  
    1.29 @@ -84,11 +84,11 @@
    1.30      }
    1.31    }
    1.32  
    1.33 -  def check_thy_text(qualifier: String, name: Document.Node.Name, text: CharSequence)
    1.34 +  def check_thy_reader(qualifier: String, name: Document.Node.Name, reader: Reader[Char])
    1.35      : Document.Node.Header =
    1.36    {
    1.37      try {
    1.38 -      val header = Thy_Header.read(text)
    1.39 +      val header = Thy_Header.read(reader).decode_symbols
    1.40  
    1.41        val base_name = Long_Name.base_name(name.theory)
    1.42        val name1 = header.name
    1.43 @@ -103,7 +103,7 @@
    1.44    }
    1.45  
    1.46    def check_thy(qualifier: String, name: Document.Node.Name): Document.Node.Header =
    1.47 -    with_thy_text(name, check_thy_text(qualifier, name, _))
    1.48 +    with_thy_reader(name, check_thy_reader(qualifier, name, _))
    1.49  
    1.50  
    1.51    /* document changes */