fun double_extra(name: JavaString, def_value: Float): Float in "Java" `{
		return self.getDoubleExtra(name, def_value);
	`}