Just a question on this: In the current file, it says:
# The search is performed half a second after the most recent event in order to prevent the search hapenning on every keypress.
# Each of the event handlers simply marks the time of the most recent event and a timer periodically executes doSearch
However, if I'm reading the code right, this isn't the case: it's doing the search every half second and every time the selection is changed, since:
def on_selection_modified(self, view):
Isn't that a bit resource intensive?