refer to internal File_Model instead of external file;
authorwenzelm
Sun Jan 08 17:22:14 2017 +0100 (2017-01-08 ago)
changeset 648374efe34df9136
parent 64836 3611f759f896
child 64838 ae6c51dcba9c
refer to internal File_Model instead of external file;
src/Tools/jEdit/src/jedit_resources.scala
     1.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Sun Jan 08 17:10:42 2017 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Sun Jan 08 17:22:14 2017 +0100
     1.3 @@ -82,9 +82,11 @@
     1.4    override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
     1.5    {
     1.6      GUI_Thread.now {
     1.7 -      JEdit_Lib.jedit_buffer(name) match {
     1.8 -        case Some(buffer) =>
     1.9 +      Document_Model.get(name) match {
    1.10 +        case Some(buffer_model: Buffer_Model) =>
    1.11 +          val buffer = buffer_model.buffer
    1.12            JEdit_Lib.buffer_lock(buffer) { Some(f(JEdit_Lib.buffer_reader(buffer))) }
    1.13 +        case Some(file_model: File_Model) => Some(f(Scan.char_reader(file_model.content.text)))
    1.14          case None => None
    1.15        }
    1.16      } getOrElse {