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))
     }
   }
 }