idris-lang/Idris-dev — pull request #1375 by david-christiansen (2014-07-10 18:25:33+00:00)
Title: 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.