Make the pretty printer configurable

[vkleen]

With #1262 we're now using the pretty printer for printing evaluated terms in the REPL. As @yannham pointed out, that means in particular that we echo entire function definitions back to the user if something evaluates to a function in the REPL. We should instead print abbreviated placeholders for these cases, such as <function>.

In other place, we do want to print full terms, however. The natural solution would to make the Pretty instances for Term for configurable, for instance implementing them for something like (Term, PrettyConfiguration).