src/Tools/jEdit/src/document_model.scala
changeset 56462 b64b0cb845fe
parent 56457 eea4bbe15745
child 56468 30128d1acfbc
equal deleted inserted replaced
56461:ae33d153f6cc 56462:b64b0cb845fe
   136   }
   136   }
   137 
   137 
   138 
   138 
   139   /* blob */
   139   /* blob */
   140 
   140 
   141   private var _blob: Option[(Bytes, Command.File)] = None  // owned by Swing thread
   141   private var _blob: Option[(Bytes, Command.Chunk.File)] = None  // owned by Swing thread
   142 
   142 
   143   private def reset_blob(): Unit = Swing_Thread.require { _blob = None }
   143   private def reset_blob(): Unit = Swing_Thread.require { _blob = None }
   144 
   144 
   145   def get_blob(): Option[Document.Blob] =
   145   def get_blob(): Option[Document.Blob] =
   146     Swing_Thread.require {
   146     Swing_Thread.require {
   149         val (bytes, file) =
   149         val (bytes, file) =
   150           _blob match {
   150           _blob match {
   151             case Some(x) => x
   151             case Some(x) => x
   152             case None =>
   152             case None =>
   153               val bytes = PIDE.resources.file_content(buffer)
   153               val bytes = PIDE.resources.file_content(buffer)
   154               val file = new Command.File(node_name.node, buffer.getSegment(0, buffer.getLength))
   154               val file =
       
   155                 new Command.Chunk.File(node_name.node, buffer.getSegment(0, buffer.getLength))
   155               _blob = Some((bytes, file))
   156               _blob = Some((bytes, file))
   156               (bytes, file)
   157               (bytes, file)
   157           }
   158           }
   158         val changed = pending_edits.is_pending()
   159         val changed = pending_edits.is_pending()
   159         Some(Document.Blob(bytes, file, changed))
   160         Some(Document.Blob(bytes, file, changed))