explicit caret position after replacement;
authorwenzelm
Sun Sep 29 18:51:01 2013 +0200 (2013-09-29 ago)
changeset 5398716a0cd5293d9
parent 53986 a269577d97c0
child 53988 1781bf24cdf1
child 53989 729700091556
explicit caret position after replacement;
src/Tools/jEdit/src/completion_popup.scala
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Sun Sep 29 16:01:22 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Sun Sep 29 18:51:01 2013 +0200
     1.3 @@ -259,6 +259,7 @@
     1.4                content.substring(0, caret - len) +
     1.5                item.replacement +
     1.6                content.substring(caret))
     1.7 +            text_field.getCaret.setDot(caret - len + item.replacement.length)
     1.8            case _ =>
     1.9          }
    1.10        }