This is a temporary thing, later there'll be some facility to let
frontends handle any annotations marked as "this is a number" (as opposed
to "this is a string") in a generic manner and display them in any
supported (by that frontend) format, e.g. ascii, hex, oct, decimal,
binary, big-endian vs. little-endian, and so on.
This is a fix related to #201.