src/Pure/PIDE/command.scala
changeset 60215 5fb4990dfc73
parent 59924 801b979ec0c2
child 60916 a6e2a667b0a8
     1.1 --- a/src/Pure/PIDE/command.scala	Fri May 01 15:33:43 2015 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Sun May 03 00:01:10 2015 +0200
     1.3 @@ -427,7 +427,7 @@
     1.4    val chunks: Map[Symbol.Text_Chunk.Name, Symbol.Text_Chunk] =
     1.5      ((Symbol.Text_Chunk.Default -> chunk) ::
     1.6        (for (Exn.Res((name, Some((_, file)))) <- blobs)
     1.7 -        yield (Symbol.Text_Chunk.File(name.node) -> file))).toMap
     1.8 +        yield Symbol.Text_Chunk.File(name.node) -> file)).toMap
     1.9  
    1.10    def length: Int = source.length
    1.11    def range: Text.Range = chunk.range