Module JavaProperties

The type of properties.

Returns a new java.util.Properties instance, with the passed defaults if not null, empty otherwise.

get_property props key returns the value of the property whose key is key in props if found, None otherwise; see getProperty(...).

get_property_default props key def returns the value of the property whose key is key in props if found, def otherwise; see getProperty(...).

string_property_names props returns the list of the keys for the properties defined in props (including defaults); see stringPropertyNames(...).

set_property props key value set the property with key key to value value in props, returning the previous value if any; see setProperty(...).

load props str loads the properties from stream str into props; see load(...).
Raises Java_exception if an i/o error occurs

load_xml props str loads the properties from stream str into props; see loadFromXML(...).
Raises Java_exception if an i/o error occurs

store props str stores the properties props onto the stream str with optional comment commment; see store(...).
Raises Java_exception if an i/o error occurs

store_to_xml props str stores the properties props onto the stream str with optional comment commment; see storeToXML(...).
Raises Java_exception if an i/o error occurs

The null value.

is_null obj returns true iff obj is equal to null.

is_not_null obj returns false iff obj is equal to null.

wrap obj wraps the reference obj into an option type:

• Some x if obj is not null;
• None if obj is null.

unwrap obj unwraps the option obj into a bare reference:

• Some x is mapped to x;
• None is mapped to null.