# HG changeset patch
# User wenzelm
# Date 1747392102 -7200
# Node ID dc7efd56454427b3356dd42203afd9015105be08
# Parent  e840461d537023bd5b2b69f6c36c35cfc8db1d87
more standard color properties, following org.gjt.sp.util.SyntaxUtilities.getColorHexString();

diff -r e840461d5370 -r dc7efd564544 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Fri May 16 12:10:49 2025 +0200
+++ b/Admin/components/components.sha1	Fri May 16 12:41:42 2025 +0200
@@ -276,6 +276,7 @@
 07360418d691f6bb0e250e8efeb6b935e23eb0cd jedit-20250423.tar.gz
 995ac4cd9086e1647f1628988884c7c135123965 jedit-20250424.tar.gz
 5637fb7b2d0c24ca4d1ffe18156d2f6a8ec9fab3 jedit-20250515.tar.gz
+62cce488b1c5541de7a56a4a49537037da2bfd44 jedit-20250516.tar.gz
 44775a22f42a9d665696bfb49e53c79371c394b0 jedit_build-20111217.tar.gz
 a242a688810f2bccf24587b0062ce8027bf77fa2 jedit_build-20120304.tar.gz
 4c948dee53f74361c097c08f49a1a5ff9b17bd1d jedit_build-20120307.tar.gz
diff -r e840461d5370 -r dc7efd564544 Admin/components/main
--- a/Admin/components/main	Fri May 16 12:10:49 2025 +0200
+++ b/Admin/components/main	Fri May 16 12:41:42 2025 +0200
@@ -15,7 +15,7 @@
 isabelle_setup-20240327
 javamail-20250122
 jdk-21.0.6
-jedit-20250515
+jedit-20250516
 jfreechart-1.5.3
 jortho-1.0-2
 jsoup-1.18.3
diff -r e840461d5370 -r dc7efd564544 src/Pure/Admin/component_jedit.scala
--- a/src/Pure/Admin/component_jedit.scala	Fri May 16 12:10:49 2025 +0200
+++ b/src/Pure/Admin/component_jedit.scala	Fri May 16 12:41:42 2025 +0200
@@ -445,57 +445,57 @@
 view.middleMousePaste=true
 view.showSearchbar=true
 view.showToolbar=false
-view.status.memory.background=#666699
+view.status.memory.background=\#ff666699
 view.status=( mode , fold , encoding ) locked wrap multiSelect rectSelect overwrite lineSep buffersets task-monitor java-status ml-status errors clock
 view.thickCaret=true
 view.width=1200
 xml-insert-closing-tag.shortcut=
 
 #dark theme
-view.bgColor.dark=\#2B2B2B
-view.caretColor.dark=\#99ff99
-view.eolMarkerColor.dark=\#ffcc00
-view.fgColor.dark=\#ffffff
-view.gutter.bgColor.dark=\#282828
-view.gutter.currentLineColor.dark=\#66cc00
-view.gutter.fgColor.dark=\#ffffff
-view.gutter.focusBorderColor.dark=\#99ccff
-view.gutter.foldColor.dark=\#838383
-view.gutter.highlightColor.dark=\#ffcc00
-view.gutter.markerColor.dark=\#006666
-view.gutter.noFocusBorderColor.dark=\#ffffff
-view.gutter.selectionAreaBgColor.dark=\#282828
-view.gutter.structureHighlightColor.dark=\#cccccc
-view.lineHighlightColor.dark=\#1d0a0a
-view.selectionColor.dark=\#0f4982
-view.status.background.dark=\#333333
-view.status.foreground.dark=\#ffffff
-view.status.memory.background.dark=\#66699a
-view.status.memory.foreground.dark=\#cccccc
-view.structureHighlightColor.dark=\#ffff00
-view.style.comment1.dark=color\:\#87ceeb
-view.style.comment2.dark=color\:\#cd5c5c
-view.style.comment3.dark=color\:\#999900
-view.style.comment4.dark=color\:\#cc6600
-view.style.digit.dark=color\:\#cc3300
-view.style.foldLine.0.dark=color\:\#ffffff bgColor\:\#452424 style\:b
-view.style.foldLine.1.dark=color\:\#ffffff bgColor\:\#625950 style\:b
-view.style.foldLine.2.dark=color\:\#ffffff bgColor\:\#3c3c67 style\:b
-view.style.foldLine.3.dark=color\:\#ffffff bgColor\:\#314444 style\:b
-view.style.function.dark=color\:\#98fb98
-view.style.invalid.dark=color\:\#ff0066 bgColor\:\#ffffcc
-view.style.keyword1.dark=color\:\#f0e68c style\:b
-view.style.keyword2.dark=color\:\#009966 style\:b
-view.style.keyword3.dark=color\:\#cc6600 style\:b
-view.style.keyword4.dark=color\:\#66ccff style\:b
-view.style.label.dark=color\:\#ffdead
-view.style.literal1.dark=color\:\#ffa0a0
-view.style.literal2.dark=color\:\#cc6600
-view.style.literal3.dark=color\:\#ffcc00
-view.style.literal4.dark=color\:\#ffffff
-view.style.markup.dark=color\:\#bdb76b
-view.style.operator.dark=color\:\#9b9b9b style\:b
-view.wrapGuideColor.dark=\#8080ff
+view.bgColor.dark=\#ff2b2b2b
+view.caretColor.dark=\#ff99ff99
+view.eolMarkerColor.dark=\#ffffcc00
+view.fgColor.dark=\#ffffffff
+view.gutter.bgColor.dark=\#ff282828
+view.gutter.currentLineColor.dark=\#ff66cc00
+view.gutter.fgColor.dark=\#ffffffff
+view.gutter.focusBorderColor.dark=\#ff99ccff
+view.gutter.foldColor.dark=\#ff838383
+view.gutter.highlightColor.dark=\#ffffcc00
+view.gutter.markerColor.dark=\#ff006666
+view.gutter.noFocusBorderColor.dark=\#ffffffff
+view.gutter.selectionAreaBgColor.dark=\#ff282828
+view.gutter.structureHighlightColor.dark=\#ffcccccc
+view.lineHighlightColor.dark=\#ff1d0a0a
+view.selectionColor.dark=\#ff0f4982
+view.status.background.dark=\#ff333333
+view.status.foreground.dark=\#ffffffff
+view.status.memory.background.dark=\#ff66699a
+view.status.memory.foreground.dark=\#ffcccccc
+view.structureHighlightColor.dark=\#ffffff00
+view.style.comment1.dark=color\:\#ff87ceeb
+view.style.comment2.dark=color\:\#ffcd5c5c
+view.style.comment3.dark=color\:\#ff999900
+view.style.comment4.dark=color\:\#ffcc6600
+view.style.digit.dark=color\:\#ffcc3300
+view.style.foldLine.0.dark=color\:\#ffffffff bgColor\:\#ff452424 style\:b
+view.style.foldLine.1.dark=color\:\#ffffffff bgColor\:\#ff625950 style\:b
+view.style.foldLine.2.dark=color\:\#ffffffff bgColor\:\#ff3c3c67 style\:b
+view.style.foldLine.3.dark=color\:\#ffffffff bgColor\:\#ff314444 style\:b
+view.style.function.dark=color\:\#ff98fb98
+view.style.invalid.dark=color\:\#ffff0066 bgColor\:\#ffffffcc
+view.style.keyword1.dark=color\:\#fff0e68c style\:b
+view.style.keyword2.dark=color\:\#ff009966 style\:b
+view.style.keyword3.dark=color\:\#ffcc6600 style\:b
+view.style.keyword4.dark=color\:\#ff66ccff style\:b
+view.style.label.dark=color\:\#ffffdead
+view.style.literal1.dark=color\:\#ffffa0a0
+view.style.literal2.dark=color\:\#ffcc6600
+view.style.literal3.dark=color\:\#ffffcc00
+view.style.literal4.dark=color\:\#ffffffff
+view.style.markup.dark=color\:\#ffbdb76b
+view.style.operator.dark=color\:\#ff9b9b9b style\:b
+view.wrapGuideColor.dark=\#ff8080ff
 """)
 
     val modes_dir = source_dir + Path.basic("modes")