src/Tools/jEdit/src/jedit_editor.scala
changeset 65187 9250f944ec0f
parent 64882 c3b42ac0cf81
child 65196 e8760a98db78
equal deleted inserted replaced
65186:4659e87c3795 65187:9250f944ec0f
    87         }
    87         }
    88         else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored)
    88         else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored)
    89       case _ =>
    89       case _ =>
    90         Document_Model.get(buffer) match {
    90         Document_Model.get(buffer) match {
    91           case Some(model) if !model.is_theory =>
    91           case Some(model) if !model.is_theory =>
    92             snapshot.version.nodes.commands_loading(model.node_name) match {
    92             snapshot.version.nodes.commands_loading(model.node_name).headOption
    93               case cmd :: _ => Some(cmd)
       
    94               case Nil => None
       
    95             }
       
    96           case _ => None
    93           case _ => None
    97         }
    94         }
    98     }
    95     }
    99   }
    96   }
   100 
    97