Feature: Decimal character preference in XML and native CSV export formats

Added a new <decimal-character> container to the preferences section of the XML output format whose content is the user's choice for decimal separator character (period or comma). Note that regardless of this setting, decimal numbers within the XML file itself always use period as the decimal separator. Appropriate declarations for this item were added to the XML Document Type Definition and CSS style sheet of this {\tt DOCTYPE}.

Added a sixth field at the end of the ``{\tt Preferences}'' header item in our native CSV export for the decimal character. Natually, this field will be quoted if the decimal character is set to comma.