src/Tools/jEdit/src/document_model.scala
changeset 56473 5b5c750e9763
parent 56469 ffc94a271633
child 56662 f373fb77e0a4
     1.1 --- a/src/Tools/jEdit/src/document_model.scala	Tue Apr 08 20:00:53 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_model.scala	Tue Apr 08 20:03:00 2014 +0200
     1.3 @@ -138,7 +138,7 @@
     1.4  
     1.5    /* blob */
     1.6  
     1.7 -  private var _blob: Option[(Bytes, Text.Chunk.File)] = None  // owned by Swing thread
     1.8 +  private var _blob: Option[(Bytes, Text.Chunk)] = None  // owned by Swing thread
     1.9  
    1.10    private def reset_blob(): Unit = Swing_Thread.require { _blob = None }
    1.11  
    1.12 @@ -146,17 +146,17 @@
    1.13      Swing_Thread.require {
    1.14        if (is_theory) None
    1.15        else {
    1.16 -        val (bytes, file) =
    1.17 +        val (bytes, chunk) =
    1.18            _blob match {
    1.19              case Some(x) => x
    1.20              case None =>
    1.21                val bytes = PIDE.resources.file_content(buffer)
    1.22 -              val file = new Text.Chunk.File(buffer.getSegment(0, buffer.getLength))
    1.23 -              _blob = Some((bytes, file))
    1.24 -              (bytes, file)
    1.25 +              val chunk = Text.Chunk(buffer.getSegment(0, buffer.getLength))
    1.26 +              _blob = Some((bytes, chunk))
    1.27 +              (bytes, chunk)
    1.28            }
    1.29          val changed = pending_edits.is_pending()
    1.30 -        Some(Document.Blob(bytes, file, changed))
    1.31 +        Some(Document.Blob(bytes, chunk, changed))
    1.32        }
    1.33      }
    1.34