The user.options used to contain the default user options as well, but this was split off into a regular module called user.defaults (stateless, cacheable) in 2015 (https://gerrit.wikimedia.org/r/177501).
What's left is a fairly small blob of JSON that is user-specific, private, and embedded into the HTML head. Which is exactly what user.tokens is as well.
Let's merge these.
Actual plan
- Merge user.tokens into user.options (Yes, we found a way. Yes, it's hacky but it's worth it as it'll be least disruptive to end-users and developers this way).
- Update uses of user.tokens to user.options in core.
- Update uses of user.tokens to user.options in WMF extensions.
- Update uses of user.tokens to user.options on WMF wikis (after the core change is deployed to all wikis).
- Write a short migration guide on https://www.mediawiki.org/wiki/ResourceLoader/Migration_guide_(users).
- Remove user.tokens in MW 1.35.