webeditor themes

Stream: general

[Jon Eugster]

The webeditor (currently only lean.math.hhu.de) has now the option to add load monaco themes. Does anybody have a favourite theme they are using which could be added as presets?

[Jon Eugster]

Utensil Song said:

A quick css hack to make https://live.lean-lang.org dark again in case anyone is also interested: https://gist.github.com/utensil/552f47cd687290c1131da0a79cc7dff9

This theme has currently been removed again, as it was plain CSS and not a monaco theme. I don't fully understand how monaco themes work and what the difference to vscode-themes is, but I'd be happy to upload this dark theme again if we get it in the correct format. (or any other theme people might have)