--- 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)
}