# HG changeset patch
# User wenzelm
# Date 1345643597 -7200
# Node ID 61dc7d5d150a94d3f680d64ea7c2d128ec39873a
# Parent  46e053eda5ddda011c98df703c2ee2df8c85ade8
use Thy_Header.read on explicit text only -- potentially via File.read, not Scan.byte_reader;
tuned signatures;

diff -r 46e053eda5dd -r 61dc7d5d150a src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Wed Aug 22 12:47:49 2012 +0200
+++ b/src/Pure/Thy/thy_header.scala	Wed Aug 22 15:53:17 2012 +0200
@@ -106,13 +106,6 @@
   def read(source: CharSequence): Thy_Header =
     read(new CharSequenceReader(source))
 
-  def read(file: JFile): Thy_Header =
-  {
-    val reader = Scan.byte_reader(file)
-    try { read(reader).map(Standard_System.decode_permissive_utf8) }
-    finally { reader.close }
-  }
-
 
   /* keywords */
 
diff -r 46e053eda5dd -r 61dc7d5d150a src/Pure/Thy/thy_load.scala
--- a/src/Pure/Thy/thy_load.scala	Wed Aug 22 12:47:49 2012 +0200
+++ b/src/Pure/Thy/thy_load.scala	Wed Aug 22 15:53:17 2012 +0200
@@ -27,13 +27,6 @@
   def append(dir: String, source_path: Path): String =
     (Path.explode(dir) + source_path).expand.implode
 
-  def read_header(name: Document.Node.Name): Thy_Header =
-  {
-    val path = Path.explode(name.node)
-    if (!path.is_file) error("No such file: " + path.toString)
-    Thy_Header.read(path.file)
-  }
-
 
   /* theory files */
 
@@ -49,8 +42,9 @@
     }
   }
 
-  def check_header(name: Document.Node.Name, header: Thy_Header): Document.Node.Header =
+  def check_thy_text(name: Document.Node.Name, text: CharSequence): Document.Node.Header =
   {
+    val header = Thy_Header.read(text)
     val name1 = header.name
     val imports = header.imports.map(import_name(name.dir, _))
     // FIXME val uses = header.uses.map(p => (append(name.dir, Path.explode(p._1)), p._2))
@@ -62,6 +56,10 @@
   }
 
   def check_thy(name: Document.Node.Name): Document.Node.Header =
-    check_header(name, read_header(name))
+  {
+    val path = Path.explode(name.node)
+    if (!path.is_file) error("No such file: " + path.toString)
+    check_thy_text(name, File.read(path))
+  }
 }
 
diff -r 46e053eda5dd -r 61dc7d5d150a src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Wed Aug 22 12:47:49 2012 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Wed Aug 22 15:53:17 2012 +0200
@@ -68,8 +68,7 @@
     Swing_Thread.require()
     Isabelle.buffer_lock(buffer) {
       Exn.capture {
-        Isabelle.thy_load.check_header(name,
-          Thy_Header.read(buffer.getSegment(0, buffer.getLength)))
+        Isabelle.thy_load.check_thy_text(name, buffer.getSegment(0, buffer.getLength))
       } match {
         case Exn.Res(header) => header
         case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))
diff -r 46e053eda5dd -r 61dc7d5d150a src/Tools/jEdit/src/jedit_thy_load.scala
--- a/src/Tools/jEdit/src/jedit_thy_load.scala	Wed Aug 22 12:47:49 2012 +0200
+++ b/src/Tools/jEdit/src/jedit_thy_load.scala	Wed Aug 22 15:53:17 2012 +0200
@@ -53,22 +53,20 @@
     }
   }
 
-  override def read_header(name: Document.Node.Name): Thy_Header =
+  override def check_thy(name: Document.Node.Name): Document.Node.Header =
   {
     Swing_Thread.now {
       Isabelle.jedit_buffer(name.node) match {
         case Some(buffer) =>
           Isabelle.buffer_lock(buffer) {
-            val text = new Segment
-            buffer.getText(0, buffer.getLength, text)
-            Some(Thy_Header.read(text))
+            Some(check_thy_text(name, buffer.getSegment(0, buffer.getLength)))
           }
         case None => None
       }
     } getOrElse {
       val file = new JFile(name.node)  // FIXME load URL via jEdit VFS (!?)
       if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
-      Thy_Header.read(file)
+      check_thy_text(name, File.read(file))
     }
   }
 }