src/Tools/jEdit/src/document_model.scala
changeset 56746 d37a5d09a277
parent 56662 f373fb77e0a4
child 56801 8dd9df88f647
--- a/src/Tools/jEdit/src/document_model.scala	Sat Apr 26 13:32:28 2014 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Sat Apr 26 13:34:10 2014 +0200
@@ -138,7 +138,7 @@
 
   /* blob */
 
-  private var _blob: Option[(Bytes, Text.Chunk)] = None  // owned by Swing thread
+  private var _blob: Option[(Bytes, Symbol.Text_Chunk)] = None  // owned by Swing thread
 
   private def reset_blob(): Unit = Swing_Thread.require { _blob = None }
 
@@ -151,7 +151,7 @@
             case Some(x) => x
             case None =>
               val bytes = PIDE.resources.file_content(buffer)
-              val chunk = Text.Chunk(buffer.getSegment(0, buffer.getLength))
+              val chunk = Symbol.Text_Chunk(buffer.getSegment(0, buffer.getLength))
               _blob = Some((bytes, chunk))
               (bytes, chunk)
           }