# HG changeset patch
# User wenzelm
# Date 1747737085 -7200
# Node ID e3a8f8694a45a315e2e22f3fbe59bffcf58ad01d
# Parent  2bb4a8d0111d64d045e4b60c4e01634fb9cc8bbc
clarified default properties -- requires to update jedit component;

diff -r 2bb4a8d0111d -r e3a8f8694a45 src/Pure/Admin/component_jedit.scala
--- a/src/Pure/Admin/component_jedit.scala	Sun May 18 14:33:01 2025 +0000
+++ b/src/Pure/Admin/component_jedit.scala	Tue May 20 12:31:25 2025 +0200
@@ -268,6 +268,7 @@
 console.encoding=UTF-8
 console.font=Isabelle DejaVu Sans Mono
 console.fontsize=14
+console.shell.default=Scala
 delete-line.shortcut=A+d
 delete.shortcut2=C+d
 """ + drop_encodings.map(a => "encoding.opt-out." + a + "=true").mkString("\n") + """
@@ -452,6 +453,12 @@
 xml-insert-closing-tag.shortcut=
 
 #dark theme
+console.bgColor.dark=\#ff000000
+console.plainColor.dark=\#ffffffff
+console.caretColor.dark=\#ffffffff
+console.infoColor.dark=\#ffc1dfee
+console.warningColor.dark=\#ffff8c00
+console.errorColor.dark=\#ffb22222
 view.bgColor.dark=\#ff2b2b2b
 view.caretColor.dark=\#ff99ff99
 view.eolMarkerColor.dark=\#ffffcc00