# HG changeset patch # User wenzelm # Date 1747342529 -7200 # Node ID 0fa6759948bc5dc3ca5ffa94628eb1846085dc96 # Parent 210be56ecd1dabc4dac436f6e2c1426822f940e4 explicit support for dark GUI themes in Isabelle/jEdit; diff -r 210be56ecd1d -r 0fa6759948bc Admin/components/components.sha1 --- a/Admin/components/components.sha1 Wed May 14 11:31:23 2025 +0200 +++ b/Admin/components/components.sha1 Thu May 15 22:55:29 2025 +0200 @@ -275,6 +275,7 @@ a291746959e64916e8504b89dca804186d4eb8a1 jedit-20250422.tar.gz 07360418d691f6bb0e250e8efeb6b935e23eb0cd jedit-20250423.tar.gz 995ac4cd9086e1647f1628988884c7c135123965 jedit-20250424.tar.gz +5637fb7b2d0c24ca4d1ffe18156d2f6a8ec9fab3 jedit-20250515.tar.gz 44775a22f42a9d665696bfb49e53c79371c394b0 jedit_build-20111217.tar.gz a242a688810f2bccf24587b0062ce8027bf77fa2 jedit_build-20120304.tar.gz 4c948dee53f74361c097c08f49a1a5ff9b17bd1d jedit_build-20120307.tar.gz diff -r 210be56ecd1d -r 0fa6759948bc Admin/components/main --- a/Admin/components/main Wed May 14 11:31:23 2025 +0200 +++ b/Admin/components/main Thu May 15 22:55:29 2025 +0200 @@ -15,7 +15,7 @@ isabelle_setup-20240327 javamail-20250122 jdk-21.0.6 -jedit-20250424 +jedit-20250515 jfreechart-1.5.3 jortho-1.0-2 jsoup-1.18.3 diff -r 210be56ecd1d -r 0fa6759948bc CONTRIBUTORS --- a/CONTRIBUTORS Wed May 14 11:31:23 2025 +0200 +++ b/CONTRIBUTORS Thu May 15 22:55:29 2025 +0200 @@ -6,6 +6,9 @@ Contributions to this Isabelle version -------------------------------------- +* February 2025: Kai Naumann and Balazs Toth, LMU München + Initial design and implementation of dark mode for Isabelle/jEdit. + * May 2025: Benoit Ballenghien contributed the simproc apply_cont to HOLCF diff -r 210be56ecd1d -r 0fa6759948bc NEWS --- a/NEWS Wed May 14 11:31:23 2025 +0200 +++ b/NEWS Thu May 15 22:55:29 2025 +0200 @@ -50,6 +50,14 @@ * GUI rendering for dark look-and-feels has been slightly improved, e.g. menu accelerator font/color. +* Explicit support for dark GUI themes: FlatLaf tells wether a Swing +look & feel is dark or non-dark (default); jEdit options with suffix +".dark" and Isabelle options with suffix "_dark" determine GUI rendering +in dark mode. The panels for "Global Options" and "Plugin Options / +Isabelle / Rendering" operate on options according to the current Swing +look & feel, e.g. on "view.fgColor.dark" in dark mode vs. "view.fgColor" +in non-dark mode. + * Provide scalable icons for old-fashioned "tango" (from early Gnome or KDE), and "idea-icons" from current IntelliJ IDEA community edition. All icons are available for jEdit and Isabelle/jEdit add-ons. The special diff -r 210be56ecd1d -r 0fa6759948bc src/Pure/Admin/component_jedit.scala --- a/src/Pure/Admin/component_jedit.scala Wed May 14 11:31:23 2025 +0200 +++ b/src/Pure/Admin/component_jedit.scala Thu May 15 22:55:29 2025 +0200 @@ -450,6 +450,52 @@ 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 """) val modes_dir = source_dir + Path.basic("modes") diff -r 210be56ecd1d -r 0fa6759948bc src/Pure/System/options.scala --- a/src/Pure/System/options.scala Wed May 14 11:31:23 2025 +0200 +++ b/src/Pure/System/options.scala Thu May 15 22:55:29 2025 +0200 @@ -111,6 +111,9 @@ val TAG_COLOR_DIALOG = "color_dialog" // special color selection dialog val TAG_VSCODE = "vscode" // relevant for "isabelle vscode" and "isabelle vscode_server" + val SUFFIX_DARK = "_dark" + def theme_suffix(): String = if (GUI.is_dark_laf()) SUFFIX_DARK else "" + case class Entry( public: Boolean, pos: Position.T, @@ -159,6 +162,8 @@ def for_build_sync: Boolean = for_tag(TAG_BUILD_SYNC) def for_vscode: Boolean = for_tag(TAG_VSCODE) + def is_dark: Boolean = name.endsWith(SUFFIX_DARK) + def session_content: Boolean = for_content || for_document } diff -r 210be56ecd1d -r 0fa6759948bc src/Tools/jEdit/etc/options --- a/src/Tools/jEdit/etc/options Wed May 14 11:31:23 2025 +0200 +++ b/src/Tools/jEdit/etc/options Thu May 15 22:55:29 2025 +0200 @@ -156,6 +156,75 @@ option markdown_bullet3_color : string = "E7E7FFFF" for color_dialog option markdown_bullet4_color : string = "FFE0F0FF" for color_dialog +option outdated_color_dark : string = "B0B0B0FF" for color_dialog +option unprocessed_color_dark : string = "D89090FF" for color_dialog +option unprocessed1_color_dark : string = "330033FF" for color_dialog +option running_color_dark : string = "7FBFFF00" for color_dialog +option running1_color_dark : string = "590259FF" for color_dialog +option bullet_color_dark : string = "EAEAEAFF" for color_dialog +option tooltip_color_dark : string = "FFFFE9FF" for color_dialog +option writeln_color_dark : string = "9C9C9CFF" for color_dialog +option information_color_dark : string = "77B800FF" for color_dialog +option warning_color_dark : string = "FF8C00FF" for color_dialog +option legacy_color_dark : string = "FF8C00FF" for color_dialog +option error_color_dark : string = "FF7070FF" for color_dialog +option ok_color_dark : string = "FFFFFFFF" for color_dialog +option failed_color_dark : string = "FF6B6BFF" for color_dialog +option writeln_message_color_dark : string = "444444FF" for color_dialog +option information_message_color_dark : string = "221E40FF" for color_dialog +option tracing_message_color_dark : string = "6969A749" for color_dialog +option warning_message_color_dark : string = "FF7A007F" for color_dialog +option legacy_message_color_dark : string = "716D4BFF" for color_dialog +option error_message_color_dark : string = "5B1220FF" for color_dialog +option spell_checker_color_dark : string = "589EF9FF" for color_dialog +option bad_color_dark : string = "620909FF" for color_dialog +option canceled_color_dark : string = "F67979FF" for color_dialog +option intensify_color_dark : string = "FFCC6664" for color_dialog +option entity_color_dark : string = "330033FF" for color_dialog +option entity_ref_color_dark : string = "E071DEFF" for color_dialog +option breakpoint_disabled_color_dark : string = "CCCC0080" for color_dialog +option breakpoint_enabled_color_dark : string = "FF9966FF" for color_dialog +option quoted_color_dark : string = "FFFFFF0C" for color_dialog +option antiquoted_color_dark : string = "EDEDED1B" for color_dialog +option antiquote_color_dark : string = "FFE4E1FF" for color_dialog +option raw_text_color_dark : string = "FFFFCCFF" for color_dialog +option plain_text_color_dark : string = "F2A558FF" for color_dialog +option highlight_color_dark : string = "50505032" for color_dialog +option hyperlink_color_dark : string = "4DD2FFFF" for color_dialog +option active_color_dark : string = "454594FF" for color_dialog +option active_hover_color_dark : string = "4A4AC9FF" for color_dialog +option active_result_color_dark : string = "A7A77BFF" for color_dialog +option keyword1_color_dark : string = "2FAEF9FF" for color_dialog +option keyword2_color_dark : string = "0EF1C9FF" for color_dialog +option keyword3_color_dark : string = "92D8FAFF" for color_dialog +option quasi_keyword_color_dark : string = "9999FFFF" for color_dialog +option improper_color_dark : string = "F99F9FFF" for color_dialog +option operator_color_dark : string = "DBDBDBFF" for color_dialog +option comment1_color_dark : string = "A7D3A2FF" for color_dialog +option comment2_color_dark : string = "E2A05AFF" for color_dialog +option comment3_color_dark : string = "75BDB3FF" for color_dialog +option caret_debugger_color_dark : string = "FF9966FF" for color_dialog +option caret_invisible_color_dark : string = "FFB8B880" for color_dialog +option completion_color_dark : string = "4BBDF7FF" for color_dialog +option search_color_dark : string = "66FFFF64" for color_dialog + +option tfree_color_dark : string = "C68CFDFF" for color_dialog +option tvar_color_dark : string = "CE8DF7FF" for color_dialog +option free_color_dark : string = "80B1FEFF" for color_dialog +option skolem_color_dark : string = "FF99FFFF" for color_dialog +option bound_color_dark : string = "76E9C6FF" for color_dialog +option var_color_dark : string = "F0A860FF" for color_dialog +option inner_numeral_color_dark : string = "FF8A8AFF" for color_dialog +option inner_quoted_color_dark : string = "FF7AE4FF" for color_dialog +option inner_cartouche_color_dark : string = "FF8A14FF" for color_dialog +option dynamic_color_dark : string = "80CB8DFF" for color_dialog +option class_parameter_color_dark : string = "E58948FF" for color_dialog + +option markdown_bullet1_color_dark : string = "181719FF" for color_dialog +option markdown_bullet2_color_dark : string = "333333FF" for color_dialog +option markdown_bullet3_color_dark : string = "000022FF" for color_dialog +option markdown_bullet4_color_dark : string = "1B000DFF" for color_dialog + section "Icons" diff -r 210be56ecd1d -r 0fa6759948bc src/Tools/jEdit/patches/extended_styles_brackets --- a/src/Tools/jEdit/patches/extended_styles_brackets Wed May 14 11:31:23 2025 +0200 +++ b/src/Tools/jEdit/patches/extended_styles_brackets Thu May 15 22:55:29 2025 +0200 @@ -82,36 +82,3 @@ default: return '\0'; } } //}}} -diff -ru jedit5.7.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java jedit5.7.0-patched/jEdit/org/gjt/sp/util/SyntaxUtilities.java ---- jedit5.7.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2024-08-03 19:53:21.000000000 +0200 -+++ jedit5.7.0-patched/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2024-10-29 11:50:54.066016546 +0100 -@@ -357,8 +357,28 @@ - } - } - -- return styles; -+ styles[0] = -+ new SyntaxStyle(org.gjt.sp.jedit.jEdit.getColorProperty("view.fgColor", Color.BLACK), -+ null, new Font(family, 0, size)); -+ return _styleExtender.extendStyles(styles); - } //}}} - -+ /** -+ * Extended styles derived from the user-specified style array. -+ */ -+ -+ public static class StyleExtender -+ { -+ public SyntaxStyle[] extendStyles(SyntaxStyle[] styles) -+ { -+ return styles; -+ } -+ } -+ volatile private static StyleExtender _styleExtender = new StyleExtender(); -+ public static void setStyleExtender(StyleExtender ext) -+ { -+ _styleExtender = ext; -+ } -+ - private SyntaxUtilities(){} - } diff -r 210be56ecd1d -r 0fa6759948bc src/Tools/jEdit/patches/gui --- a/src/Tools/jEdit/patches/gui Wed May 14 11:31:23 2025 +0200 +++ b/src/Tools/jEdit/patches/gui Thu May 15 22:55:29 2025 +0200 @@ -1,6 +1,6 @@ diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/GUIUtilities.java --- jedit5.7.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java 2024-08-03 19:53:15.000000000 +0200 -+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/GUIUtilities.java 2025-04-23 14:28:53.149349418 +0200 ++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/GUIUtilities.java 2025-05-14 11:07:16.919569611 +0200 @@ -42,6 +42,8 @@ import java.net.URL; import java.util.*; @@ -90,7 +90,7 @@ FontRenderContext frc = new FontRenderContext(null, true, false); float scale = font1.getLineMetrics("", frc).getHeight() / font2.getLineMetrics("", frc).getHeight(); -@@ -1107,6 +1124,22 @@ +@@ -1107,6 +1124,48 @@ //{{{ Colors and styles @@ -100,7 +100,7 @@ + "MenuItem.acceleratorSelectionForeground" : + "MenuItem.acceleratorForeground"); + -+ if (color == null) color = Color.black; ++ if (color == null) color = defaultFgColor(); + + return color; + } @@ -110,10 +110,47 @@ + return com.formdev.flatlaf.FlatLaf.isLafDark(); + } + ++ public static Color defaultBgColor() ++ { ++ return isDarkLaf() ? Color.BLACK : Color.WHITE; ++ } ++ ++ public static Color defaultFgColor() ++ { ++ return isDarkLaf() ? Color.WHITE : Color.BLACK; ++ } ++ ++ public static String getTheme() ++ { ++ return isDarkLaf() ? "dark" : ""; ++ } ++ ++ public static String getThemeSuffix() ++ { ++ return getThemeSuffix("."); ++ } ++ ++ public static String getThemeSuffix(String s) ++ { ++ String t = getTheme(); ++ return t.isEmpty() ? t : s + t; ++ } ++ //{{{ getStyleString() method /** * Converts a style into it's string representation. -@@ -1619,6 +1652,21 @@ +@@ -1407,8 +1466,8 @@ + { + for (Component child: win.getComponents()) + { +- child.setBackground(jEdit.getColorProperty("view.bgColor", Color.WHITE)); +- child.setForeground(jEdit.getColorProperty("view.fgColor", Color.BLACK)); ++ child.setBackground(jEdit.getColorProperty("view.bgColor", defaultBgColor())); ++ child.setForeground(jEdit.getColorProperty("view.fgColor")); + if (child instanceof JTextPane) + ((JTextPane)child).setUI(new javax.swing.plaf.basic.BasicEditorPaneUI()); + if (child instanceof Container) +@@ -1619,6 +1678,21 @@ } //}}} @@ -645,7 +682,7 @@ #}}} diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/options/BrowserColorsOptionPane.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/options/BrowserColorsOptionPane.java --- jedit5.7.0/jEdit/org/gjt/sp/jedit/options/BrowserColorsOptionPane.java 2024-08-03 19:53:15.000000000 +0200 -+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/options/BrowserColorsOptionPane.java 2025-04-16 16:12:29.542089148 +0200 ++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/options/BrowserColorsOptionPane.java 2025-05-14 10:51:38.322378673 +0200 @@ -78,12 +78,12 @@ buttons.setBorder(new EmptyBorder(3,0,0,0)); buttons.setLayout(new BoxLayout(buttons,BoxLayout.X_AXIS)); @@ -676,6 +713,16 @@ moveDown.setToolTipText(jEdit.getProperty("common.moveDown")); moveDown.addActionListener(actionHandler); buttons.add(moveDown); +@@ -209,8 +209,7 @@ + { + entries.add(new Entry(glob, + jEdit.getColorProperty( +- "vfs.browser.colors." + i + ".color", +- Color.black))); ++ "vfs.browser.colors." + i + ".color"))); + i++; + } + } //}}} diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/options/StatusBarOptionPane.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/options/StatusBarOptionPane.java --- jedit5.7.0/jEdit/org/gjt/sp/jedit/options/StatusBarOptionPane.java 2024-08-03 19:53:15.000000000 +0200 +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/options/StatusBarOptionPane.java 2025-04-16 16:12:37.730958557 +0200 @@ -715,3 +762,330 @@ clearRegister.setToolTipText(GenericGUIUtilities.prettifyMenuLabel( jEdit.getProperty("clear-string-register.label"))); clearRegister.addActionListener(e -> clearSelectedIndex()); +diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/jEdit.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/jEdit.java +--- jedit5.7.0/jEdit/org/gjt/sp/jedit/jEdit.java 2024-08-03 19:53:14.000000000 +0200 ++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/jEdit.java 2025-05-15 21:20:18.075698848 +0200 +@@ -674,6 +674,12 @@ + return value; + } //}}} + ++ public static String getThemeProperty(String name) ++ { ++ String s = GUIUtilities.getThemeSuffix(); ++ return s.isEmpty() ? getProperty(name) : getProperty(name + s, getProperty(name)); ++ } ++ + //{{{ getProperty() method + /** + * Returns the property with the specified name.

+@@ -859,7 +865,7 @@ + */ + public static Color getColorProperty(String name) + { +- return getColorProperty(name,Color.black); ++ return getColorProperty(name, GUIUtilities.defaultFgColor()); + } + + /** +@@ -870,7 +876,7 @@ + */ + public static Color getColorProperty(String name, Color def) + { +- String value = getProperty(name); ++ String value = getThemeProperty(name); + if(value == null) + return def; + else +@@ -886,7 +892,7 @@ + */ + public static void setColorProperty(String name, Color value) + { +- setProperty(name, SyntaxUtilities.getColorHexString(value)); ++ setThemeProperty(name, SyntaxUtilities.getColorHexString(value)); + } //}}} + + //{{{ getColorMatrixProperty() method +@@ -936,6 +942,11 @@ + public static void setProperty(String name, String value) + { + propMgr.setProperty(name,value); ++ } ++ ++ public static void setThemeProperty(String name, String value) ++ { ++ setProperty(name + GUIUtilities.getThemeSuffix(), value); + } //}}} + + //{{{ setTemporaryProperty() method +@@ -4233,7 +4244,7 @@ + } //}}} + + //{{{ gotoMarker() method +- private static void gotoMarker(final View view, final Buffer buffer, ++ public static void gotoMarker(final View view, final Buffer buffer, + final String marker) + { + AwtRunnableQueue.INSTANCE.runAfterIoTasks(new Runnable() +diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/BufferSwitcher.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/BufferSwitcher.java +--- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/BufferSwitcher.java 2024-08-03 19:53:16.000000000 +0200 ++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/BufferSwitcher.java 2025-05-13 16:29:14.196283445 +0200 +@@ -58,7 +58,7 @@ + public static final DataFlavor BufferDataFlavor = new DataFlavor(BufferTransferableData.class, DataFlavor.javaJVMLocalObjectMimeType); + + // actual colors will be set in constructor, here are just fallback values +- static Color defaultColor = Color.BLACK; ++ static Color defaultColor = GUIUtilities.defaultFgColor(); + static Color defaultBGColor = Color.LIGHT_GRAY; + + public BufferSwitcher(final EditPane editPane) +diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/LogViewer.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/LogViewer.java +--- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/LogViewer.java 2024-08-03 19:53:16.000000000 +0200 ++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/LogViewer.java 2025-05-14 11:05:39.544481221 +0200 +@@ -413,7 +413,7 @@ + { + this.list = list; + debugColor = jEdit.getColorProperty("log-viewer.message.debug.color", Color.BLUE); +- messageColor = jEdit.getColorProperty("log-viewer.message.message.color", Color.BLACK); ++ messageColor = jEdit.getColorProperty("log-viewer.message.message.color"); + noticeColor = jEdit.getColorProperty("log-viewer.message.notice.color", Color.GREEN); + warningColor = jEdit.getColorProperty("log-viewer.message.warning.color", Color.ORANGE); + errorColor = jEdit.getColorProperty("log-viewer.message.error.color", Color.RED); +diff -ru /home/makarius/.isabelle/contrib/jedit-20250424/jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/io/VFS.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/io/VFS.java +--- /home/makarius/.isabelle/contrib/jedit-20250424/jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/io/VFS.java 2024-08-03 19:53:14.000000000 +0200 ++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/io/VFS.java 2025-05-14 10:51:16.530755624 +0200 +@@ -1302,8 +1302,7 @@ + colors.add(new ColorEntry( + Pattern.compile(StandardUtilities.globToRE(glob)), + jEdit.getColorProperty( +- "vfs.browser.colors." + i + ".color", +- Color.black))); ++ "vfs.browser.colors." + i + ".color"))); + } + catch(PatternSyntaxException e) + { +diff -ru jedit5.7.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java jedit5.7.0-patched/jEdit/org/gjt/sp/util/SyntaxUtilities.java +--- jedit5.7.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2024-08-03 19:53:21.000000000 +0200 ++++ jedit5.7.0-patched/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2025-05-14 15:20:40.515623017 +0200 +@@ -35,6 +35,7 @@ + import org.gjt.sp.jedit.syntax.SyntaxStyle; + import org.gjt.sp.jedit.syntax.Token; + import org.gjt.sp.jedit.IPropertyManager; ++import org.gjt.sp.jedit.GUIUtilities; + + import static java.util.stream.Collectors.joining; + //}}} +@@ -49,6 +50,15 @@ + public class SyntaxUtilities + { + public static IPropertyManager propertyManager; ++ ++ public static String getThemeProperty(String name) ++ { ++ String s = GUIUtilities.getThemeSuffix(); ++ String a = propertyManager.getProperty(name); ++ String b = propertyManager.getProperty(name + s); ++ return b == null ? a : b; ++ } ++ + private static final Pattern COLOR_MATRIX_PATTERN = Pattern.compile("(?x)\n" + + "^\n" + + "\\s*+ # optionally preceded by whitespace\n" + +@@ -125,7 +135,7 @@ + */ + public static Color parseColor(String name) + { +- return parseColor(name, Color.black); ++ return parseColor(name, GUIUtilities.defaultFgColor()); + } //}}} + + //{{{ parseColor() method +@@ -267,7 +277,7 @@ + if(s.startsWith("color:")) + { + if(color) +- fgColor = parseColor(s.substring(6), Color.black); ++ fgColor = parseColor(s.substring(6), GUIUtilities.defaultFgColor()); + } + else if(s.startsWith("bgColor:")) + { +@@ -311,7 +321,7 @@ + boolean color) + throws IllegalArgumentException + { +- return parseStyle(str, family, size, color, Color.black); ++ return parseStyle(str, family, size, color, GUIUtilities.defaultFgColor()); + } //}}} + + //{{{ loadStyles() methods +@@ -347,9 +357,7 @@ + String styleName = "view.style." + + Token.tokenToString((byte)i) + .toLowerCase(Locale.ENGLISH); +- styles[i] = parseStyle( +- propertyManager.getProperty(styleName), +- family,size,color); ++ styles[i] = parseStyle(getThemeProperty(styleName),family,size,color); + } + catch(Exception e) + { +@@ -357,8 +365,28 @@ + } + } + +- return styles; ++ styles[0] = ++ new SyntaxStyle(org.gjt.sp.jedit.jEdit.getColorProperty("view.fgColor", GUIUtilities.defaultFgColor()), ++ null, new Font(family, 0, size)); ++ return _styleExtender.extendStyles(styles); + } //}}} + ++ /** ++ * Extended styles derived from the user-specified style array. ++ */ ++ ++ public static class StyleExtender ++ { ++ public SyntaxStyle[] extendStyles(SyntaxStyle[] styles) ++ { ++ return styles; ++ } ++ } ++ volatile private static StyleExtender _styleExtender = new StyleExtender(); ++ public static void setStyleExtender(StyleExtender ext) ++ { ++ _styleExtender = ext; ++ } ++ + private SyntaxUtilities(){} + } +diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/EditPane.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/EditPane.java +--- jedit5.7.0/jEdit/org/gjt/sp/jedit/EditPane.java 2024-08-03 19:53:15.000000000 +0200 ++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/EditPane.java 2025-05-14 15:46:36.934878462 +0200 +@@ -43,6 +43,7 @@ + import org.gjt.sp.jedit.msg.BufferChanging; + import org.gjt.sp.jedit.msg.BufferUpdate; + import org.gjt.sp.jedit.msg.EditPaneUpdate; ++import org.gjt.sp.jedit.msg.PositionChanging; + import org.gjt.sp.jedit.msg.PropertiesChanged; + import org.gjt.sp.jedit.options.GeneralOptionPane; + import org.gjt.sp.jedit.options.GutterOptionPane; +@@ -380,9 +381,11 @@ + buffer.unsetProperty(Buffer.CARET_POSITIONED); + + +- if(caret != -1) ++ if(caret != -1) { + textArea.setCaretPosition(Math.min(caret, + buffer.getLength())); ++ EditBus.send(new PositionChanging(this)); ++ } + + // set any selections + Selection[] selection = caretInfo.selection; +@@ -1029,7 +1032,7 @@ + for(int i = 0; i <= 3; i++) + { + foldLineStyle[i] = SyntaxUtilities.parseStyle( +- jEdit.getProperty("view.style.foldLine." + i), ++ jEdit.getThemeProperty("view.style.foldLine." + i), + defaultFont,defaultFontSize, true); + } + painter.setFoldLineStyle(foldLineStyle); +diff -ru /home/makarius/.isabelle/contrib/jedit-20250424/jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/NumericTextField.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/NumericTextField.java +--- /home/makarius/.isabelle/contrib/jedit-20250424/jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/NumericTextField.java 2024-08-03 19:53:18.000000000 +0200 ++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/NumericTextField.java 2025-05-14 15:46:44.805742407 +0200 +@@ -95,7 +95,7 @@ + Font font = getFont(); + String family = font.getFamily(); + int size = font.getSize(); +- invalidStyle = SyntaxUtilities.parseStyle(jEdit.getProperty("view.style.invalid"), family, size, true); ++ invalidStyle = SyntaxUtilities.parseStyle(jEdit.getThemeProperty("view.style.invalid"), family, size, true); + defaultForeground = getForeground(); + defaultBackground = getBackground(); + } +diff -ru /home/makarius/.isabelle/contrib/jedit-20250424/jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/statusbar/ErrorsWidgetFactory.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/statusbar/ErrorsWidgetFactory.java +--- /home/makarius/.isabelle/contrib/jedit-20250424/jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/statusbar/ErrorsWidgetFactory.java 2024-08-03 19:53:16.000000000 +0200 ++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/statusbar/ErrorsWidgetFactory.java 2025-05-14 15:46:52.413610804 +0200 +@@ -102,7 +102,7 @@ + String defaultFont = jEdit.getProperty("view.font"); + int defaultFontSize = jEdit.getIntegerProperty("view.fontsize", 12); + SyntaxStyle invalid = SyntaxUtilities.parseStyle( +- jEdit.getProperty("view.style.invalid"), ++ jEdit.getThemeProperty("view.style.invalid"), + defaultFont,defaultFontSize, true); + foregroundColor = invalid.getForegroundColor(); + setForeground(foregroundColor); +diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/options/SyntaxHiliteOptionPane.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/options/SyntaxHiliteOptionPane.java +--- jedit5.7.0/jEdit/org/gjt/sp/jedit/options/SyntaxHiliteOptionPane.java 2024-08-03 19:53:15.000000000 +0200 ++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/options/SyntaxHiliteOptionPane.java 2025-05-15 21:23:50.047418219 +0200 +@@ -222,8 +222,7 @@ + { + for (StyleChoice ch : styleChoices) + { +- jEdit.setProperty(ch.property, +- GUIUtilities.getStyleString(ch.style)); ++ jEdit.setThemeProperty(ch.property,GUIUtilities.getStyleString(ch.style)); + } + } //}}} + +@@ -233,7 +232,7 @@ + Font font = new JLabel().getFont(); + styleChoices.add(new StyleChoice(label, + property, +- SyntaxUtilities.parseStyle(jEdit.getProperty(property), ++ SyntaxUtilities.parseStyle(jEdit.getThemeProperty(property), + font.getFamily(), font.getSize(), true))); + } //}}} + +@@ -289,8 +288,8 @@ + else + { + // this part sucks +- setBackground(jEdit.getColorProperty( +- "view.bgColor")); ++ setBackground( ++ jEdit.getColorProperty("view.bgColor", GUIUtilities.defaultBgColor())); + } + setFont(style.getFont()); + } +diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java +--- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java 2024-08-03 19:53:18.000000000 +0200 ++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java 2025-05-14 15:48:00.821423396 +0200 +@@ -90,12 +90,12 @@ + String property = "view.style." + typeName.toLowerCase(); + Font font = new JLabel().getFont(); + SyntaxStyle currentStyle = SyntaxUtilities.parseStyle( +- jEdit.getProperty(property), font.getFamily(), font.getSize(), true); ++ jEdit.getThemeProperty(property), font.getFamily(), font.getSize(), true); + SyntaxStyle style = new StyleEditor(textArea.getView(), + currentStyle, typeName).getStyle(); + if(style != null) + { +- jEdit.setProperty(property, GUIUtilities.getStyleString(style)); ++ jEdit.setProperty(property + GUIUtilities.getThemeSuffix(), GUIUtilities.getStyleString(style)); + jEdit.propertiesChanged(); + } + } //}}} +diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/search/SearchBar.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/search/SearchBar.java +--- jedit5.7.0/jEdit/org/gjt/sp/jedit/search/SearchBar.java 2024-08-03 19:53:18.000000000 +0200 ++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/search/SearchBar.java 2025-05-14 15:49:19.228054251 +0200 +@@ -51,6 +51,10 @@ + setFloatable(false); + add(Box.createHorizontalStrut(2)); + ++ if (!jEdit.getProperty("navigate-toolbar", "").isEmpty()) { ++ add(GUIUtilities.loadToolBar("navigate-toolbar")); ++ } ++ + JLabel label = new JLabel(jEdit.getProperty("view.search.find")); + add(label); + +@@ -59,7 +63,7 @@ + add(find = new HistoryTextField("find")); + find.setSelectAllOnFocus(true); + +- SyntaxStyle style = SyntaxUtilities.parseStyle(jEdit.getProperty("view.style.invalid"), "Dialog", 12, true); ++ SyntaxStyle style = SyntaxUtilities.parseStyle(jEdit.getThemeProperty("view.style.invalid"), "Dialog", 12, true); + errorBackground = style.getBackgroundColor(); + errorForeground = style.getForegroundColor(); + defaultBackground = find.getBackground(); diff -r 210be56ecd1d -r 0fa6759948bc src/Tools/jEdit/patches/position_changing --- a/src/Tools/jEdit/patches/position_changing Wed May 14 11:31:23 2025 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,24 +0,0 @@ -diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/EditPane.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/EditPane.java ---- jedit5.7.0/jEdit/org/gjt/sp/jedit/EditPane.java 2024-08-03 19:53:15.000000000 +0200 -+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/EditPane.java 2025-04-24 11:45:26.809862122 +0200 -@@ -43,6 +43,7 @@ - import org.gjt.sp.jedit.msg.BufferChanging; - import org.gjt.sp.jedit.msg.BufferUpdate; - import org.gjt.sp.jedit.msg.EditPaneUpdate; -+import org.gjt.sp.jedit.msg.PositionChanging; - import org.gjt.sp.jedit.msg.PropertiesChanged; - import org.gjt.sp.jedit.options.GeneralOptionPane; - import org.gjt.sp.jedit.options.GutterOptionPane; -@@ -380,9 +381,11 @@ - buffer.unsetProperty(Buffer.CARET_POSITIONED); - - -- if(caret != -1) -+ if(caret != -1) { - textArea.setCaretPosition(Math.min(caret, - buffer.getLength())); -+ EditBus.send(new PositionChanging(this)); -+ } - - // set any selections - Selection[] selection = caretInfo.selection; diff -r 210be56ecd1d -r 0fa6759948bc src/Tools/jEdit/patches/search_bar --- a/src/Tools/jEdit/patches/search_bar Wed May 14 11:31:23 2025 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,14 +0,0 @@ -diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/search/SearchBar.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/search/SearchBar.java ---- jedit5.7.0/jEdit/org/gjt/sp/jedit/search/SearchBar.java 2024-08-03 19:53:18.000000000 +0200 -+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/search/SearchBar.java 2025-04-03 11:33:23.921426197 +0200 -@@ -51,6 +51,10 @@ - setFloatable(false); - add(Box.createHorizontalStrut(2)); - -+ if (!jEdit.getProperty("navigate-toolbar", "").isEmpty()) { -+ add(GUIUtilities.loadToolBar("navigate-toolbar")); -+ } -+ - JLabel label = new JLabel(jEdit.getProperty("view.search.find")); - add(label); - diff -r 210be56ecd1d -r 0fa6759948bc src/Tools/jEdit/patches/vfs_marker --- a/src/Tools/jEdit/patches/vfs_marker Wed May 14 11:31:23 2025 +0200 +++ b/src/Tools/jEdit/patches/vfs_marker Thu May 15 22:55:29 2025 +0200 @@ -69,15 +69,3 @@ //{{{ getPath() method public String getPath() { -diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/jEdit.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/jEdit.java ---- jedit5.7.0/jEdit/org/gjt/sp/jedit/jEdit.java 2024-08-03 19:53:14.000000000 +0200 -+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/jEdit.java 2024-10-29 11:50:54.062016616 +0100 -@@ -4233,7 +4233,7 @@ - } //}}} - - //{{{ gotoMarker() method -- private static void gotoMarker(final View view, final Buffer buffer, -+ public static void gotoMarker(final View view, final Buffer buffer, - final String marker) - { - AwtRunnableQueue.INSTANCE.runAfterIoTasks(new Runnable() diff -r 210be56ecd1d -r 0fa6759948bc src/Tools/jEdit/src/jedit_options.scala --- a/src/Tools/jEdit/src/jedit_options.scala Wed May 14 11:31:23 2025 +0200 +++ b/src/Tools/jEdit/src/jedit_options.scala Thu May 15 22:55:29 2025 +0200 @@ -124,10 +124,12 @@ } class Isabelle_Rendering_Options extends Isabelle_Options("isabelle-rendering") { + val is_dark = GUI.is_dark_laf() + private val predefined = (for { opt <- PIDE.options.value.iterator - if opt.for_color_dialog + if opt.for_color_dialog && opt.is_dark == is_dark } yield PIDE.options.make_color_component(opt)).toList assert(predefined.nonEmpty) @@ -138,7 +140,7 @@ } class JEdit_Options(init_options: Options) extends Options_Variable(init_options) { - def color_value(s: String): Color = Color_Value(string(s)) + def color_value(s: String): Color = Color_Value(string(s + Options.theme_suffix())) def make_color_component(opt: Options.Entry): JEdit_Options.Entry = { GUI_Thread.require {} diff -r 210be56ecd1d -r 0fa6759948bc src/Tools/jEdit/src/jedit_rendering.scala --- a/src/Tools/jEdit/src/jedit_rendering.scala Wed May 14 11:31:23 2025 +0200 +++ b/src/Tools/jEdit/src/jedit_rendering.scala Thu May 15 22:55:29 2025 +0200 @@ -166,7 +166,7 @@ def color(s: String): Color = if (s == "main_color") main_color - else Color_Value(options.string(s)) + else Color_Value(options.string(s + Options.theme_suffix())) def color(c: Rendering.Color.Value): Color = _rendering_colors(c) diff -r 210be56ecd1d -r 0fa6759948bc src/Tools/jEdit/src/pretty_text_area.scala --- a/src/Tools/jEdit/src/pretty_text_area.scala Wed May 14 11:31:23 2025 +0200 +++ b/src/Tools/jEdit/src/pretty_text_area.scala Thu May 15 22:55:29 2025 +0200 @@ -156,7 +156,7 @@ for (i <- 0 to 3) { fold_line_style(i) = SyntaxUtilities.parseStyle( - jEdit.getProperty("view.style.foldLine." + i), + jEdit.getThemeProperty("view.style.foldLine." + i), current_font_info.family, current_font_info.size.round, true) } getPainter.setFoldLineStyle(fold_line_style)