diff -r 4659e87c3795 -r 9250f944ec0f src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Sat Mar 11 15:36:47 2017 +0100 +++ b/src/Pure/PIDE/document.scala Sat Mar 11 16:22:12 2017 +0100 @@ -857,9 +857,9 @@ { val former_range = revert(range).inflate_singularity val (chunk_name, command_iterator) = - commands_loading match { - case command :: _ => (Symbol.Text_Chunk.File(node_name.node), Iterator((command, 0))) - case _ => (Symbol.Text_Chunk.Default, node.command_iterator(former_range)) + commands_loading.headOption match { + case None => (Symbol.Text_Chunk.Default, node.command_iterator(former_range)) + case Some(command) => (Symbol.Text_Chunk.File(node_name.node), Iterator((command, 0))) } val markup_index = Command.Markup_Index(status, chunk_name) (for {