--- a/src/Tools/jEdit/src/document_model.scala Wed Aug 22 15:53:17 2012 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Wed Aug 22 16:10:23 2012 +0200
@@ -68,7 +68,8 @@
Swing_Thread.require()
Isabelle.buffer_lock(buffer) {
Exn.capture {
- Isabelle.thy_load.check_thy_text(name, buffer.getSegment(0, buffer.getLength))
+ val text = buffer.getSegment(0, buffer.getLength)
+ Isabelle.thy_load.check_thy_text(session.recent_syntax, name, text)
} match {
case Exn.Res(header) => header
case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))