fun get_int(key: JavaString, def_value: Int): Int in "Java" `{
		int return_value;
		try {
			return_value = self.getInt(key, (int)def_value);
		} catch (ClassCastException e) {
			return def_value;
		}

		return return_value;
	`}