GUI tools

The "Tools" menu allows to:

• serialize a configuration file with the current state of the GUI options
• Unserialize a configuration file and update the state of the GUI options
• Reset the state of the GUI options to their default values
• Export the CSS file specifying the default StyleSheet theme

Serializing a configuration file

The Tools menu "Save Configuration File" option allows to generate a configuration file with the current state of the GUI interface options.

Unserializing a configuration file

The Tools menu "Apply Configuration File" option allows to use a previously saved configuration file and update the state of the options.

Note that another way to Unserialize the configuration File is to set the "Additional Configuration" fields in the Properties area in the GUI with the previously saved configuration :

Reset the GUI options

The Tools menu "Set Configuration" option allows to update the state of the options to their respective default value.

Export the CSS file specifying the default StyleSheet theme

The Tools menu "Export Theme" allows to export the the default StyleSheet theme in a CSS file.