indexing
	description: "parent of all Java array classes that contains the common routines to all arrays. Not to be used directly, instead use the class with array of specific type."

class interface
	JAVA_ARRAY

create

feature 

	count: INTEGER
			-- number of cells in this array

	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_from_pointer (p: POINTER)
			-- make an Eiffel array accessor out of a pointer to a
			-- Java array
		require
			valid: p /= default_pointer

	valid_index (index: INTEGER): BOOLEAN
			-- index is valid if it's between 0..count-1
	
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

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

end -- class JAVA_ARRAY