Changing font size

[frios]

If I want to change the default font size, what is the best way to do that? I tried to create a new theme with a different font size to pass into the CodeEditor call, but I get

'Theme' initializer is inaccessible due to 'internal' protection level

I don't see any other obvious way to make that change.

Thanks

[mchakravarty]

Sorry for the late response. I have now made the components of Theme public (it was an oversight that I didn't do that right away). The properties are now also mutable; i.e., you can simply change the font size of an existing theme if that is what you want (or you create a new one). I hope this helps.