more tolerant treatment of end-of-buffer -- avoid debatable situations of jEdit buffer boundaries;

--- 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
       }
     }