changeset 65187 | 9250f944ec0f |
parent 64882 | c3b42ac0cf81 |
child 65196 | e8760a98db78 |
--- 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 } }