clarified colors for "dark" theme -- requires to update jedit component;
authorwenzelm
Wed, 21 May 2025 17:42:38 +0200
changeset 82657 249701eeea76
parent 82656 1db11efcd355
child 82658 5f985cda3095
clarified colors for "dark" theme -- requires to update jedit component;
src/Pure/Admin/component_jedit.scala
--- a/src/Pure/Admin/component_jedit.scala	Wed May 21 16:34:03 2025 +0200
+++ b/src/Pure/Admin/component_jedit.scala	Wed May 21 17:42:38 2025 +0200
@@ -474,10 +474,12 @@
 view.gutter.selectionAreaBgColor.dark=\#ff282828
 view.gutter.structureHighlightColor.dark=\#ffcccccc
 view.lineHighlightColor.dark=\#ff1d0a0a
+view.multipleSelectionColor.dark=\#ff006622
 view.selectionColor.dark=\#ff0f4982
 view.status.background.dark=\#ff333333
 view.status.foreground.dark=\#ffffffff
-view.status.memory.background.dark=\#ff66699a
+view.status.highlight.dark=\#ff141414
+view.status.memory.background.dark=\#ff666699
 view.status.memory.foreground.dark=\#ffcccccc
 view.structureHighlightColor.dark=\#ffffff00
 view.style.comment1.dark=color\:\#ff87ceeb