Remove --measureTime from FormattingOptions

It doesn’t really belong there, as it concerns only the command-line
tool, not the formatting library. Now, the command-line tool will
extract it directly.