# HG changeset patch
# User wenzelm
# Date 1380035592 -7200
# Node ID 08721d7b22628e9688328b1863d383d3b52c7fa2
# Parent  71f103629327b463929bb0e7ffe4eb864a8876ce
more tolerant treatment of end-of-buffer -- avoid debatable situations of jEdit buffer boundaries;

diff -r 71f103629327 -r 08721d7b2262 src/Tools/jEdit/src/jedit_editor.scala
--- 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
       }
     }