# HG changeset patch
# User wenzelm
# Date 1489245732 -3600
# Node ID 9250f944ec0f8da9853ec7ea4ae89f38f0f686a4
# Parent  4659e87c379569a0112647a9d01810860764eb5d
tuned;

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 {
diff -r 4659e87c3795 -r 9250f944ec0f src/Tools/jEdit/src/jedit_editor.scala
--- 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
         }
     }