indexing
description: "Holds information abouy JNI environment. Potentially many JNI environments can exists at once, but more than one was never tested"
class interface
JNI_ENVIRONMENT
create
feature
destroy_vm
find_class (name: STRING): JAVA_CLASS
require
name_valid: name /= void
find_class_by_pointer (classp: POINTER): JAVA_CLASS
require
classp /= default_pointer
find_class_pointer (name: STRING): POINTER
feature
check_for_exceptions
throw_custom_exception (jclass: JAVA_CLASS; msg: STRING)
throw_java_exception (jthrowable: JAVA_OBJECT)
feature
c_check_for_exceptions (lenv: POINTER)
JAVA_EXTERNALS
c_throw_custom_exception (lenv: POINTER; jclass_id: POINTER; msg: POINTER)
JAVA_EXTERNALS
c_throw_java_exception (lenv: POINTER; jthrowable: POINTER)
JAVA_EXTERNALS
feature
attach_current_thread
detach_current_thread
invariant
ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
end -- JNI_ENVIRONMENT