# HG changeset patch
# User wenzelm
# Date 1747752747 -7200
# Node ID 692feb5e45e6335182f469a0a1af58c8db86433d
# Parent  8be3035c82d4816fd060258e2d90b32cbeb901a8
more robust Global Options panel: re-init OptionPane after switch, e.g. after change of "lookAndFeel" and re-init of GutterOptionPane, which implicitly depends on com.formdev.flatlaf.FlatLaf.isLafDark() -- requires to update jedit component;

diff -r 8be3035c82d4 -r 692feb5e45e6 src/Tools/jEdit/patches/gui
--- a/src/Tools/jEdit/patches/gui	Tue May 20 16:24:45 2025 +0200
+++ b/src/Tools/jEdit/patches/gui	Tue May 20 16:52:27 2025 +0200
@@ -1112,3 +1112,25 @@
  		drop_button.addActionListener(new DropActionHandler());
  		box.add(arrow_button);
  		box.add(drop_button);
+diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/OptionsDialog.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/OptionsDialog.java
+--- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/OptionsDialog.java	2024-08-03 19:53:18.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/OptionsDialog.java	2025-05-20 16:27:48.111088672 +0200
+@@ -191,6 +191,7 @@
+ 
+ 						if(optionPane != null)
+ 						{
++							deferredOptionPanes.clear();
+ 							deferredOptionPanes.put(
+ 								node,optionPane);
+ 						}
+diff -ru jedit5.7.0/jEdit/org/jedit/options/OptionGroupPane.java jedit5.7.0-patched/jEdit/org/jedit/options/OptionGroupPane.java
+--- jedit5.7.0/jEdit/org/jedit/options/OptionGroupPane.java	2024-08-03 19:53:23.000000000 +0200
++++ jedit5.7.0-patched/jEdit/org/jedit/options/OptionGroupPane.java	2025-05-20 16:34:10.010928214 +0200
+@@ -151,6 +151,7 @@
+ 
+ 						if (optionPane != null)
+ 						{
++							deferredOptionPanes.clear();
+ 							deferredOptionPanes.put(node, optionPane);
+ 						}
+ 						else