src/Tools/jEdit/src/document_model.scala
changeset 56823 37be55461dbe
parent 56801 8dd9df88f647
child 57610 518e28a7c74b
--- 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))