--- a/src/Tools/jEdit/src/document_model.scala Fri May 02 12:27:40 2014 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Fri May 02 13:52:45 2014 +0200
@@ -70,7 +70,7 @@
if (is_theory) {
JEdit_Lib.buffer_lock(buffer) {
Exn.capture {
- PIDE.resources.check_thy_text("", node_name, buffer.getSegment(0, buffer.getLength))
+ PIDE.resources.check_thy_reader("", node_name, JEdit_Lib.buffer_reader(buffer))
} match {
case Exn.Res(header) => header
case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))