Remove theia option in settings

[gtsiolis]

Problem to solve

Now that we're deprecating the old editor (Theia) (see #4459), we can safely remove the editor (Default IDE) preference in settings once the deprecation has been made.

⚠️ Warning: This is currently blocked until the deprecation is complete and will most probably be ready-for-development in the next milestone. /cc @akosyakov

[gtsiolis]

Since today (Sep 1), the message we have in Preferences (/preferences) for deprecating Theia is running a bit late. 😅

[csweichel]

/schedule

[roboquat]

@csweichel: Issue scheduled in the meta team (WIP: 0)

In response to this:

/schedule

Instructions for interacting with me using PR comments are available here. If you have questions or suggestions related to my behavior, please file an issue against the kubernetes/test-infra repository.

[csweichel]

/assign @laushinka