diff -r 0b7656c5f0e9 -r 5fb4990dfc73 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Fri May 01 15:33:43 2015 +0200 +++ b/src/Pure/PIDE/command.scala Sun May 03 00:01:10 2015 +0200 @@ -427,7 +427,7 @@ val chunks: Map[Symbol.Text_Chunk.Name, Symbol.Text_Chunk] = ((Symbol.Text_Chunk.Default -> chunk) :: (for (Exn.Res((name, Some((_, file)))) <- blobs) - yield (Symbol.Text_Chunk.File(name.node) -> file))).toMap + yield Symbol.Text_Chunk.File(name.node) -> file)).toMap def length: Int = source.length def range: Text.Range = chunk.range