Pretty-print signatures in hover and #check <ident>

[Kha]

Resolves #375

I changed #check to use the signature pretty printer as well mostly for testing, though I don't think there's any real downside. In fact I would probably go further and just make #check $n:ident a semantically separate command that shows the signature of n without elaboration - I can't be the only one that usually starts with #check toString and then only remembers to add the @ on the second try.

[Kha]

In fact I would probably go further and just make #check $n:ident a semantically separate command that shows the signature of n without elaboration - I can't be the only one that usually starts with #check toString and then only remembers to add the @ on the second try.

Done, https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60.23check.20.3Cident.3E.60 was generally in support

[gebner]

The only thing I'm concerned about in this PR is the abuse of the delaborator to produce something which is not a term.

[Kha]

The only thing I'm concerned about in this PR is the abuse of the delaborator to produce something which is not a term.

In contrast to other proposals like a special pp option we're not really going through the term elaborator but mostly using it from the outside, with the exception of using delabCore once for convenience. Looking at it again though, it might have been nicer to reuse only the part around creating the Delaborator.State as most of the other parts are not applicable.