Remove `History.mask`

I am wondering about the usefulness of History.mask. As far as I understood, it was necessary as long as we needed the possibility to forcefully overwrite flags, but as we changed politics to always overwrite flags no matter of their values, I am wondering, if we could ditch the mask altogether @palmb ?