Output float number with hex format

Hi!

In C Language, there is a way to format float numbers into a hex string by
using "%a" in printf.
eg:
the value: 1.2345 can be expressed as '0x1.3c083126e978dp+0' which is the
hex representation of a float number.

I have tried this in Postgres:
SELECT '0x1.3c083126e978dp+0'::float;
float8
--------
1.2345
(1 row)
This means that Postgres can accepty hex float as *input*. However I cannot
find any format function for *output*.
to_char(..., ...) does not have "%a"-like format. Is there any way to do
that?

Thank you in advance.

--
ShenLei