Add search history

In fact, there was already an embryonic search history, but it was almost useless in practice. This gives it the properties one would expect:

• distinguish search and replace histories;
• share the search history between the search bar and the replace dialog;
• update histories for each new search or replace from an explicit user action;
• add a parameter to control the size of the history;
• persistence of history between sessions (via GSettings).