src/Pure/PIDE/document.scala
changeset 56462 b64b0cb845fe
parent 56398 15d0821c8667
child 56468 30128d1acfbc
     1.1 --- a/src/Pure/PIDE/document.scala	Tue Apr 08 10:24:42 2014 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Tue Apr 08 12:19:33 2014 +0200
     1.3 @@ -45,7 +45,7 @@
     1.4  
     1.5    /* document blobs: auxiliary files */
     1.6  
     1.7 -  sealed case class Blob(bytes: Bytes, file: Command.File, changed: Boolean)
     1.8 +  sealed case class Blob(bytes: Bytes, file: Command.Chunk.File, changed: Boolean)
     1.9    {
    1.10      def unchanged: Blob = copy(changed = false)
    1.11    }
    1.12 @@ -731,15 +731,15 @@
    1.13            status: Boolean = false): List[Text.Info[A]] =
    1.14          {
    1.15            val former_range = revert(range)
    1.16 -          val (file_name, command_iterator) =
    1.17 +          val (chunk_name, command_iterator) =
    1.18              load_commands match {
    1.19 -              case command :: _ => (node_name.node, Iterator((command, 0)))
    1.20 -              case _ => ("", node.command_iterator(former_range))
    1.21 +              case command :: _ => (Command.Chunk.File_Name(node_name.node), Iterator((command, 0)))
    1.22 +              case _ => (Command.Chunk.Self, node.command_iterator(former_range))
    1.23              }
    1.24 -          val markup_index = Command.Markup_Index(status, file_name)
    1.25 +          val markup_index = Command.Markup_Index(status, chunk_name)
    1.26            (for {
    1.27              (command, command_start) <- command_iterator
    1.28 -            chunk <- command.chunks.get(file_name).iterator
    1.29 +            chunk <- command.chunks.get(chunk_name).iterator
    1.30              states = state.command_states(version, command)
    1.31              res = result(states)
    1.32              range = (former_range - command_start).restrict(chunk.range)