Pretty printing option record

This is a refactoring that replaces the bool imp flag with a pretty printing option record. This is a first step in making the pretty printing options more granular, currently showimplicit actually means "show in the most verbose way possible" (for example it turns on printing absolute names as well).

I'm not quite sure about naming and style here, so comments on that would be welcome.