src/Pure/PIDE/document.scala
changeset 56473 5b5c750e9763
parent 56470 8eda56033203
child 56475 710dee42b3d0
     1.1 --- a/src/Pure/PIDE/document.scala	Tue Apr 08 20:00:53 2014 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Tue Apr 08 20:03:00 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: Text.Chunk.File, changed: Boolean)
     1.8 +  sealed case class Blob(bytes: Bytes, chunk: Text.Chunk, changed: Boolean)
     1.9    {
    1.10      def unchanged: Blob = copy(changed = false)
    1.11    }
    1.12 @@ -774,7 +774,7 @@
    1.13            val former_range = revert(range)
    1.14            val (chunk_name, command_iterator) =
    1.15              load_commands match {
    1.16 -              case command :: _ => (Text.Chunk.File_Name(node_name.node), Iterator((command, 0)))
    1.17 +              case command :: _ => (Text.Chunk.File(node_name.node), Iterator((command, 0)))
    1.18                case _ => (Text.Chunk.Default, node.command_iterator(former_range))
    1.19              }
    1.20            val markup_index = Command.Markup_Index(status, chunk_name)