Simple completion support

The Idris REPL can now complete a single identifier or command.
Complete multiple identifiers in one expression
Complete arguments of commands (though slightly crudely)

Module names are not yet completed.
Disentangle Haskeline from the internals Idris

Now, only the areas that actually work with the user involve the InputT monad
transformer. The practical advantage of this is that different Haskeline
settings structures can be used for different shells - the main REPL, the
prover, and the TT shell, simply by providing a different completion function
in the runInputT call.
Rename the REPL's Haskeline uses to make them obviously REPL-specific
Complete tactic names in prover
Crude support for completion in prover

The prover can use the local proof state and the global environment for
completion. Right now, it doesn't always stop completing when it
should (f.x. tactics that take an already defined name are being completed
with whole expressions) but it's already useful.
Manually track prover history

Prover history is now taken care of manually to avoid adding the current proof
state to the IState record, while still having completion for assumptions.
Merge pull request #180 from david-christiansen/completion-work

Basic completion now works at REPL and in prover