options: make first (default) options for all enums Nothing

This means default options can actually be overridden both on the
command-line and in an options section/profile.
bump version to 0.7.1.5
actually use modified options record for write options!

This meant that e.g. options set in the profile or options header were
not being used when writing (e.g. table of contents).