indexing
	description: "Access to Java array of doubles"

class interface
	JAVA_DOUBLE_ARRAY

create 

	make (size: INTEGER)
			-- create a new Java array and an Eiffel accessor object
			-- Note: Java arrays are indexed from zero
		require
			size_ok: size > 0
		ensure
			array_ok: jarray /= default_pointer

feature 

	count: INTEGER
			-- number of cells in this array
			-- (from JAVA_ARRAY)

	item (index: INTEGER): DOUBLE
			-- item at "index"
		require
			valid_index (index)

	jni: JNI_ENVIRONMENT
			-- returns the standard JNI enviroment. It uses the value of
			-- CLASS_PATH environment variable to initialize the JVM
			-- (from SHARED_JNI_ENVIRONMENT)
		ensure -- from SHARED_JNI_ENVIRONMENT
			Result /= void

	make (size: INTEGER)
			-- create a new Java array and an Eiffel accessor object
			-- Note: Java arrays are indexed from zero
		require
			size_ok: size > 0
		ensure
			array_ok: jarray /= default_pointer

	make_from_pointer (p: POINTER)
			-- make an Eiffel array accessor out of a pointer to a
			-- Java array
			-- (from JAVA_ARRAY)
		require -- from JAVA_ARRAY
			valid: p /= default_pointer

	put (litem: DOUBLE; index: INTEGER)
			-- replace item at "index"
		require
			valid_index (index)

	valid_index (index: INTEGER): BOOLEAN
			-- index is valid if it's between 0..count-1
			-- (from JAVA_ARRAY)
	
feature -- Java exception mechanism

	c_check_for_exceptions (lenv: POINTER)
			-- (from JAVA_EXTERNALS)

	c_throw_custom_exception (lenv: POINTER; jclass_id: POINTER; msg: POINTER)
			-- (from JAVA_EXTERNALS)

	c_throw_java_exception (lenv: POINTER; jthrowable: POINTER)
			-- (from JAVA_EXTERNALS)
	
invariant

		-- from ANY
	reflexive_equality: standard_is_equal (Current)
	reflexive_conformance: conforms_to (Current)
		-- from JAVA_ARRAY
	jarray /= default_pointer

end -- class JAVA_DOUBLE_ARRAY