Advanced preferences

We might need to modify the keybinding to permit falling back to use of keyCodes (see ). Does Theia have the concept of “advanced” preferences, preferences that are rarely used, risky, or nitty-gritty, and so not normally displayed to the user unless they elect to see them?

[original thread by Gabriel Bodeen]

No we don’t have such concepts.

We distinguish 2 kind of users: end users and adopters. End users are dealing with usual preferences. Adopters are responsible to integrate Theia in own environments, so they can use the dependency injection vis custom extensions as primary means to run it the best, so such integration time configurations are not exposed to end users.