Add an optional depth to 'search' tactic

Also add it to Language.Reflection.  It's now good enough to work with
the proof obligations in Effects, so replace the old proof search (it's
also noticeably faster in larger programs).

Requires ibcs to be rebuilt.
Add :loadto command

Loads an input file up to the declaration beginning at the given line,
discarding any declaration after that.

This only really makes sense when developing interactively: it means you
can work on something at the top of a file without worrying about how it
affects what happens later (this also potentially makes it a lot
quicker!)

Latest idris-vim uses this.
IDESlave support for setting the depth of interactive proof search
Check that proof steps introduce no new problems

In interactive mode only (it is important that proofs can fail
temporarily during elaboration since futher information may help refine
the goal).

Fixes #1243
Merge pull request #1251 from david-christiansen/ideslave-proof-depth

IDESlave support for setting the depth of interactive proof search
IDESlave support for :loadto
Merge pull request #1253 from david-christiansen/load-to-ideslave

IDESlave support for :loadto