explicit caret position after replacement;

--- a/src/Tools/jEdit/src/completion_popup.scala	Sun Sep 29 16:01:22 2013 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Sun Sep 29 18:51:01 2013 +0200
@@ -259,6 +259,7 @@
               content.substring(0, caret - len) +
               item.replacement +
               content.substring(caret))
+            text_field.getCaret.setDot(caret - len + item.replacement.length)
           case _ =>
         }
       }