Show type information in a buffer

Previously, types were shown using `message'. Now, they are shown in
their own info buffer, which lasts longer. This is particularly useful
for the types of metavariables, which show an entire proof context.