Create new PP backend annotations for literals (strings, numbers, ...)

Use these to emit string literals via a \HOLStringLit macro that can
be redefined to get better output than my default. Of course, it's
quite possible that my \textrm{``#1''} is not even a reasonable
default.

Note how the HOLStringLit macro is given an argument that doesn't have
the quotation mark delimiters around it.