fun get_int(key: JavaString): Int in "Java" `{ return self.getInt(key); `}