--- 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 {
--- a/src/Tools/jEdit/src/jedit_editor.scala Sat Mar 11 15:36:47 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala Sat Mar 11 16:22:12 2017 +0100
@@ -89,10 +89,7 @@
case _ =>
Document_Model.get(buffer) match {
case Some(model) if !model.is_theory =>
- snapshot.version.nodes.commands_loading(model.node_name) match {
- case cmd :: _ => Some(cmd)
- case Nil => None
- }
+ snapshot.version.nodes.commands_loading(model.node_name).headOption
case _ => None
}
}