# HG changeset patch
# User wenzelm
# Date 1747842158 -7200
# Node ID 249701eeea76bffcc85319d8f3c359ef783ada4b
# Parent  1db11efcd355aef40833cf4f901939c489a18e3f
clarified colors for "dark" theme -- requires to update jedit component;

diff -r 1db11efcd355 -r 249701eeea76 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