src/Pure/PIDE/resources.scala

 
 package isabelle
 
 
 import scala.annotation.tailrec
+import scala.util.parsing.input.Reader
 
 import java.io.{File => JFile}
 
 
 object Resources

   /* file-system operations */
 
   def append(dir: String, source_path: Path): String =
     (Path.explode(dir) + source_path).expand.implode
 
-  def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A =
+  def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
   {
     val path = Path.explode(name.node)
     if (!path.is_file) error("No such file: " + path.toString)
 
-    val text = File.read(path)
-    Symbol.decode_strict(text)
-    f(text)
+    val reader = Scan.byte_reader(path.file)
+    try { f(reader) } finally { reader.close }
   }
 
 
   /* theory files */
 

           Document.Node.Name(node, master_dir, Long_Name.qualify(qualifier, theory))
         }
     }
   }
 
-  def check_thy_text(qualifier: String, name: Document.Node.Name, text: CharSequence)
+  def check_thy_reader(qualifier: String, name: Document.Node.Name, reader: Reader[Char])
     : Document.Node.Header =
   {
     try {
-      val header = Thy_Header.read(text)
+      val header = Thy_Header.read(reader).decode_symbols
 
       val base_name = Long_Name.base_name(name.theory)
       val name1 = header.name
       if (base_name != name1)
         error("Bad file name " + Resources.thy_path(Path.basic(base_name)) +

     }
     catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
   }
 
   def check_thy(qualifier: String, name: Document.Node.Name): Document.Node.Header =
-    with_thy_text(name, check_thy_text(qualifier, name, _))
+    with_thy_reader(name, check_thy_reader(qualifier, name, _))
 
 
   /* document changes */
 
   def parse_change(