explicit support for dark GUI themes in Isabelle/jEdit;

--- 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

--- 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

--- 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
 
 

--- 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

--- 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")

--- 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
   }
 

--- 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"
 

--- 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(){}
- }

--- 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.<p>
+@@ -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();

--- 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;

--- 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);
- 		

--- 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()

--- 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 {}

--- 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)
 

--- 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)