Make type search work in the prover

This patch does two things:

1. It adds support for a new prover command, :search, with the same
syntax and semantics as the REPL command

2. It makes :search work properly with IDESlave, enabling type search
from the Emacs prover as well as enabling length-limits in the IRC bot
again.