Function java_double 

pub fn java_double(f: f64) -> String

A float as Java’s Double.toString writes it: 1.0, 0.001, 1.0E7, 1.0E-4, Infinity, NaN, with the shortest digits that read back the same.