Settings defined in editor plugins are missing (about 100 of them),
but all other settings (about 200 of them) can now be documented in the
EditorSettings class.
Co-authored-by: Rémi Verschelde <rverschelde@gmail.com>
(cherry picked from commit 63ce655e75e9d46c8b588ff258c3f50d5290c553)