--- a/src/Tools/jEdit/src/jedit_editor.scala Tue Sep 24 16:35:01 2013 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala Tue Sep 24 17:13:12 2013 +0200
@@ -72,12 +72,16 @@
PIDE.document_view(text_area) match {
case Some(doc_view) =>
val node = snapshot.version.nodes(doc_view.model.node_name)
- val caret_commands = node.command_range(text_area.getCaretPosition)
- if (caret_commands.hasNext) {
- val (cmd0, _) = caret_commands.next
- node.commands.reverse.iterator(cmd0).find(cmd => !cmd.is_ignored)
+ val caret = text_area.getCaretPosition
+ if (caret < text_area.getBuffer.getLength) {
+ val caret_commands = node.command_range(caret)
+ if (caret_commands.hasNext) {
+ val (cmd0, _) = caret_commands.next
+ node.commands.reverse.iterator(cmd0).find(cmd => !cmd.is_ignored)
+ }
+ else None
}
- else None
+ else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored)
case None => None
}
}