--- a/src/Pure/PIDE/document.scala Tue Apr 08 20:00:53 2014 +0200
+++ b/src/Pure/PIDE/document.scala Tue Apr 08 20:03:00 2014 +0200
@@ -45,7 +45,7 @@
/* document blobs: auxiliary files */
- sealed case class Blob(bytes: Bytes, file: Text.Chunk.File, changed: Boolean)
+ sealed case class Blob(bytes: Bytes, chunk: Text.Chunk, changed: Boolean)
{
def unchanged: Blob = copy(changed = false)
}
@@ -774,7 +774,7 @@
val former_range = revert(range)
val (chunk_name, command_iterator) =
load_commands match {
- case command :: _ => (Text.Chunk.File_Name(node_name.node), Iterator((command, 0)))
+ case command :: _ => (Text.Chunk.File(node_name.node), Iterator((command, 0)))
case _ => (Text.Chunk.Default, node.command_iterator(former_range))
}
val markup_index = Command.Markup_Index(status, chunk_name)