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