// Found the line!
editor.edit.select(c, c);
dispose();
+ editor.edit.requestFocus();
return;
}
}
// the cursor + 1, and select it
int pos = edittxt.indexOf(findtxt,
editor.edit.getSelectionStart()+1);
+ if (pos < 0) {
+ // Not found .. but try wrap-around
+ pos = edittxt.indexOf(findtxt, 0);
+ }
if (pos < 0)
new ErrorWindow(filemgr.text("edit_notfound", findtxt));
- else
+ else {
editor.edit.select(pos, pos+findtxt.length());
+ editor.edit.requestFocus();
+ }
}
else if (b == replace_b) {
// If the word to search for is selected, replace it. Otherwise