fun get_double_with_def_value(key: JavaString, def_value: Float): Float in "Java" `{
		return self.getDouble(key, def_value);
	`}