org.gjt.sp.jedit.gui.FilteredListModel.setFilter(String)