refer to internal File_Model instead of external file;
authorwenzelm
Sun, 08 Jan 2017 17:22:14 +0100
changeset 64837 4efe34df9136
parent 64836 3611f759f896
child 64838 ae6c51dcba9c
refer to internal File_Model instead of external file;
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 {