Serialize original TT terms, and annotate pretty-printer output

This allows IDEs to do things like request fully-explicit versions or normalised versions of eg terms that occur in error messages and proof contexts