# HG changeset patch
# User wenzelm
# Date 1483892534 -3600
# Node ID 4efe34df91369cca72dd4f91619e340598010e17
# Parent  3611f759f89692a6fc80a8bf44a5fa90b7ab46c2
refer to internal File_Model instead of external file;

diff -r 3611f759f896 -r 4efe34df9136 src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Sun Jan 08 17:10:42 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Sun Jan 08 17:22:14 2017 +0100
@@ -82,9 +82,11 @@
   override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
   {
     GUI_Thread.now {
-      JEdit_Lib.jedit_buffer(name) match {
-        case Some(buffer) =>
+      Document_Model.get(name) match {
+        case Some(buffer_model: Buffer_Model) =>
+          val buffer = buffer_model.buffer
           JEdit_Lib.buffer_lock(buffer) { Some(f(JEdit_Lib.buffer_reader(buffer))) }
+        case Some(file_model: File_Model) => Some(f(Scan.char_reader(file_model.content.text)))
         case None => None
       }
     } getOrElse {