fun put_double_array(key: JavaString, value: Array[Float])
	  import Array[Float].length, Array[Float].[] in "Java" `{
		double[] java_array = new double[(int)Array_of_Float_length(value)];

		for(int i=0; i < java_array.length; ++i)
			java_array[i] = Array_of_Float__index(value, i);

		self.putDoubleArray(key, java_array);
	`}