Add an option for alternate decimal notations

[nowthis]

Allow users to choose a dot or a comma as the Decimal mark. While we're here, also allow users to choose a Thousands separator of a comma or space or dot.

(I picked these options as the most commonly-used ones from https://en.wikipedia.org/wiki/Decimal_mark#Examples_of_use )

Look out for: someone picking the same item from both menus, if implemented as separate menus.

Simpler might be to just provide some constrained options in one Number Style dropdown, like this:

• 1,234.56
• 1.234,56
• 1 234,56
• 1 234.56
• 1234.56
• 1234,56

[nowthis]

7e0c4ef7e0a7aed159829ac41f93e9de4ccd25ef adds this feature