Jonathan Lindegaard Starup (Mar 11 2024 at 10:24): Jonathan Lindegaard Starup (Mar 11 2024 at 10:24):Quick question: I hope this is not the wrong place, but when I change the colors of JEdit, the hover and output state don't use the current background color. I'm trying to achieve dark mode, but no matter if I do it manually or use EditorScheme, the issue persists. Using JEdit text settings for all text elements makes no difference, either.
Yosuke Ito (Mar 12 2024 at 02:20):I am currently unable to grasp your problem precisely, but this website might help you.
https://github.com/bruderjakob17/isabelle_dark_theme
Sorry if this is not what you want.
Last updated: May 02 2024 at 12:29 UTC