--- a/src/Pure/PIDE/document.scala Tue Apr 08 10:24:42 2014 +0200
+++ b/src/Pure/PIDE/document.scala Tue Apr 08 12:19:33 2014 +0200
@@ -45,7 +45,7 @@
/* document blobs: auxiliary files */
- sealed case class Blob(bytes: Bytes, file: Command.File, changed: Boolean)
+ sealed case class Blob(bytes: Bytes, file: Command.Chunk.File, changed: Boolean)
{
def unchanged: Blob = copy(changed = false)
}
@@ -731,15 +731,15 @@
status: Boolean = false): List[Text.Info[A]] =
{
val former_range = revert(range)
- val (file_name, command_iterator) =
+ val (chunk_name, command_iterator) =
load_commands match {
- case command :: _ => (node_name.node, Iterator((command, 0)))
- case _ => ("", node.command_iterator(former_range))
+ case command :: _ => (Command.Chunk.File_Name(node_name.node), Iterator((command, 0)))
+ case _ => (Command.Chunk.Self, node.command_iterator(former_range))
}
- val markup_index = Command.Markup_Index(status, file_name)
+ val markup_index = Command.Markup_Index(status, chunk_name)
(for {
(command, command_start) <- command_iterator
- chunk <- command.chunks.get(file_name).iterator
+ chunk <- command.chunks.get(chunk_name).iterator
states = state.command_states(version, command)
res = result(states)
range = (former_range - command_start).restrict(chunk.range)