src/Tools/jEdit/src/completion_popup.scala
changeset 55666 cc350eb1087e
parent 55616 25a7a998852a
child 55690 d73949233c2e
equal deleted inserted replaced
55665:4381a2b622ea 55666:cc350eb1087e
    85           val caret = text_area.getCaretPosition
    85           val caret = text_area.getCaretPosition
    86           JEdit_Lib.try_get_text(buffer, Text.Range(caret - len, caret)) match {
    86           JEdit_Lib.try_get_text(buffer, Text.Range(caret - len, caret)) match {
    87             case Some(text) if text == item.original =>
    87             case Some(text) if text == item.original =>
    88               buffer.remove(caret - len, len)
    88               buffer.remove(caret - len, len)
    89               buffer.insert(caret - len, item.replacement)
    89               buffer.insert(caret - len, item.replacement)
       
    90               if (item.move != 0)
       
    91                 text_area.moveCaretPosition(text_area.getCaretPosition + item.move)
    90             case _ =>
    92             case _ =>
    91           }
    93           }
    92         }
    94         }
    93       }
    95       }
    94     }
    96     }
   263           case Some(text) if text == item.original =>
   265           case Some(text) if text == item.original =>
   264             text_field.setText(
   266             text_field.setText(
   265               content.substring(0, caret - len) +
   267               content.substring(0, caret - len) +
   266               item.replacement +
   268               item.replacement +
   267               content.substring(caret))
   269               content.substring(caret))
   268             text_field.getCaret.setDot(caret - len + item.replacement.length)
   270             text_field.getCaret.setDot(caret - len + item.replacement.length + item.move)
   269           case _ =>
   271           case _ =>
   270         }
   272         }
   271       }
   273       }
   272     }
   274     }
   273 
   275