search.js used to do a lot more, but now that most of the
functionality has been moved to the remote search system,
it doesn't do a lot. Merge searchDisplay.js into it.