diff -r ae33d153f6cc -r b64b0cb845fe src/Pure/PIDE/document.scala --- 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)