format = get_u32 ();
value = get_double ();
fprintf (stream, "<number value=\"%.*g\" format=\"%s%d.%d\"/>\n",
DBL_DIG, value, format_to_string(format >> 16), (format >> 8) & 0xff, format & 0xff);
format = get_u32 ();
value = get_double ();
fprintf (stream, "<number value=\"%.*g\" format=\"%s%d.%d\"/>\n",
DBL_DIG, value, format_to_string(format >> 16), (format >> 8) & 0xff, format & 0xff);