Quelle  main

diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/syntax/Chunk.java
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2024-08-03 19:53:18.000000000 +0200
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2024-10-29 11:50:54.066016546 +0100
@@ -332,9 +332,9 @@
  //{{{ Package private members
 
  //{{{ Instance variables
- SyntaxStyle style;
+ public SyntaxStyle style;
  // set up after init()
- float width;
+ public float width;
  //}}}
 
  //{{{ Chunk constructor
@@ -584,8 +584,8 @@
  // this is either style.getBackgroundColor() or
  // styles[defaultID].getBackgroundColor()
  private Color background;
- private char[] chars;
- private String str;
+ public char[] chars;
+ public String str;
  private GlyphData glyphData;
  //}}}
 
@@ -926,6 +926,11 @@
   }
 
   @Override
+  public GlyphData computeIfAbsent(GlyphKey key, java.util.function.Function<? super GlyphKey, ? extends GlyphData> f) {
+   synchronized (this) { return super.computeIfAbsent(key, f); }
+  }
+
+  @Override
   protected boolean removeEldestEntry(Map.Entry<GlyphKey, GlyphData> eldest)
   {
    return size() > capacity;
diff -Nru jedit5.7.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextArea.java
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2024-08-03 19:53:18.000000000 +0200
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2025-08-24 16:31:35.254675884 +0200
@@ -87,7 +87,9 @@
   //{{{ Initialize some misc. stuff
   selectionManager = new SelectionManager(this);
   chunkCache = new ChunkCache(this);
-  painter = new TextAreaPainter(this);
+  TextAreaPainterFactory painterFactory =
+   ServiceManager.getService(TextAreaPainterFactory.class, "painter-factory");
+  painter = painterFactory == null ? new TextAreaPainter(this) : painterFactory.create(this);
   elasticTabstopsExpander = new ElasticTabstopsTabExpander(this);
   gutter = new Gutter(this);
   gutter.setMouseActionsProvider(new MouseActions(propertyManager, "gutter"));
@@ -919,6 +921,11 @@
   return chunkCache.getLineInfo(screenLine).physicalLine;
  } //}}}
 
+        public Chunk getChunksOfScreenLine(int screenLine)
+        {
+                return chunkCache.getLineInfo(screenLine).chunks;
+        }
+
  //{{{ getScreenLineOfOffset() method
  /**
   * Returns the screen (wrapped) line containing the specified offset.
@@ -1627,8 +1634,8 @@
   }
 
   // Scan backwards, trying to find a bracket
-  String openBrackets = "([{«‹⟨⌈⌊⦇⟦⦃⟪";
-  String closeBrackets = ")]}»›⟩⌉⌋⦈⟧⦄⟫";
+  String openBrackets = "([{«‹⟨⌈⌊⦇⟦⦃⟪⦉";
+  String closeBrackets = ")]}»›⟩⌉⌋⦈⟧⦄⟫⦊";
   int count = 1;
   char openBracket = '\0';
   char closeBracket = '\0';
@@ -4983,6 +4990,7 @@
  final Point offsetXY;
 
  boolean lastLinePartial;
+ public boolean isLastLinePartial() { return lastLinePartial; }
 
  boolean blink;
  //}}}
@@ -6297,7 +6305,7 @@
   private final BreakIterator charBreaker;
   private final int index0Offset;
 
-  LineCharacterBreaker(TextArea textArea, int offset)
+  public LineCharacterBreaker(TextArea textArea, int offset)
   {
    final int line = textArea.getLineOfOffset(offset);
    charBreaker = BreakIterator.getCharacterInstance();
@@ -6348,12 +6356,12 @@
   // This class adapt CharSequence, which is used to avoid
   // text copy, to CharacterIterator, which is used to pass
   // a text to BreakIterator.
-  private static class CharIterator implements CharacterIterator
+  public static class CharIterator implements CharacterIterator
   {
    private final CharSequence sequence;
    private int index;
 
-   CharIterator(CharSequence sequence)
+   public CharIterator(CharSequence sequence)
    {
     this.sequence = sequence;
     index = 0;
@@ -6455,17 +6463,17 @@
   } //}}}
  } //}}}
 
- private int getPrevCharacterOffset(int offset)
+ public int getPrevCharacterOffset(int offset)
  {
   return new LineCharacterBreaker(this, offset).previousOf(offset);
  }
 
- private int getNextCharacterOffset(int offset)
+ public int getNextCharacterOffset(int offset)
  {
   return new LineCharacterBreaker(this, offset).nextOf(offset);
  }
 
- private int getCharacterBoundaryAt(int offset)
+ public int getCharacterBoundaryAt(int offset)
  {
   final LineCharacterBreaker charBreaker =
    new LineCharacterBreaker(this, offset);
diff -Nru jedit5.7.0/jEdit/org/gjt/sp/jedit/textarea/TextAreaPainterFactory.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextAreaPainterFactory.java
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/textarea/TextAreaPainterFactory.java 1970-01-01 01:00:00.000000000 +0100
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextAreaPainterFactory.java 2025-08-23 12:23:21.088223187 +0200
@@ -0,0 +1,9 @@
+package org.gjt.sp.jedit.textarea;
+
+public class TextAreaPainterFactory
+{
+    public TextAreaPainter create(TextArea textArea)
+    {
+        return new TextAreaPainter(textArea);
+    }
+}
diff -Nru jedit5.7.0/jEdit/org/gjt/sp/jedit/textarea/TextAreaPainter.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextAreaPainter.java
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/textarea/TextAreaPainter.java 2024-08-03 19:53:18.000000000 +0200
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextAreaPainter.java 2025-08-23 12:44:12.625895785 +0200
@@ -994,7 +994,7 @@
   * Creates a new painter. Do not create instances of this class
   * directly.
   */
- TextAreaPainter(TextArea textArea)
+ public TextAreaPainter(TextArea textArea)
  {
   enableEvents(AWTEvent.FOCUS_EVENT_MASK
    | AWTEvent.KEY_EVENT_MASK
diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/TextUtilities.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/TextUtilities.java
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 2024-08-03 19:53:20.000000000 +0200
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/TextUtilities.java 2024-10-29 11:50:54.066016546 +0100
@@ -115,6 +115,8 @@
   case '⦄': if (direction != null) direction[0] = false; return '⦃';
   case '⟪': if (direction != null) direction[0] = true;  return '⟫';
   case '⟫': if (direction != null) direction[0] = false; return '⟪';
+  case '⦉': if (direction != null) direction[0] = true;  return '⦊';
+  case '⦊': if (direction != null) direction[0] = false; return '⦉';
   default:  return '\0';
   }
  } //}}}
diff -Nru 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-08-23 15:00:39.272121361 +0200
@@ -42,6 +42,8 @@
 import java.net.URL;
 import java.util.*;
 import java.util.List;
+import java.util.regex.Pattern;
+import java.util.regex.Matcher;
 import java.lang.ref.SoftReference;
 
 import javax.annotation.Nonnull;
@@ -72,6 +74,8 @@
 import java.util.concurrent.ScheduledExecutorService;
 import java.util.concurrent.TimeUnit;
 import java.util.concurrent.atomic.AtomicLong;
+
+import com.formdev.flatlaf.extras.FlatSVGIcon;
 //}}}
 
 /** Various GUI utility functions related to icons, menus, toolbars, keyboard shortcuts, etc.
@@ -115,14 +119,14 @@
   * @return the icon
   * @since jEdit 2.6pre7
   */
- public static Icon loadIcon(String iconName)
+ public static Icon loadIcon(String iconSpec)
  {
-  if(iconName == null)
+  if(iconSpec == null)
    return null;
 
   // * Enable old icon naming scheme support
-  if(deprecatedIcons.containsKey(iconName))
-   iconName = deprecatedIcons.get(iconName);
+  if(deprecatedIcons.containsKey(iconSpec))
+   iconSpec = deprecatedIcons.get(iconSpec);
 
   // check if there is a cached version first
   Map<String, Icon> cache = null;
@@ -135,12 +139,25 @@
    cache = new HashMap<>();
    iconCache = new SoftReference<>(cache);
   }
-  Icon icon = cache.get(iconName);
+  Icon icon = cache.get(iconSpec);
   if(icon != null)
    return icon;
 
   URL url;
 
+  float iconScale = 1.0f;
+   String iconName = iconSpec;
+       {
+         Matcher matcher = Pattern.compile("^([^?]+)\\?scale=(.+)$").matcher(iconSpec);
+         if (matcher.matches()) {
+          try {
+           iconScale = Float.valueOf(matcher.group(2));
+           iconName = matcher.group(1);
+          }
+          catch (NumberFormatException e) { }
+         }
+        }
+
   try
   {
    // get the icon
@@ -164,9 +181,11 @@
    }
   }
 
-  icon = new ImageIcon(url);
+  icon =
+   url.toString().endsWith(".svg") ?
+    new FlatSVGIcon(url).derive(iconScale) : new ImageIcon(url);
 
-  cache.put(iconName,icon);
+  cache.put(iconSpec,icon);
   return icon;
  } //}}}
 
@@ -1094,9 +1113,7 @@
     return new Font("Monospaced", Font.PLAIN, 12);
    }
    else {
-    Font font2 =
-     new Font(OperatingSystem.isWindows() ? "Lucida Console" : "Monospaced",
-      Font.PLAIN, font1.getSize());
+    Font font2 = new Font("Isabelle DejaVu Sans Mono", Font.PLAIN, font1.getSize());
     FontRenderContext frc = new FontRenderContext(null, true, false);
     float scale =
      font1.getLineMetrics("", frc).getHeight() / font2.getLineMetrics("", frc).getHeight();
@@ -1107,6 +1124,48 @@
 
  //{{{ Colors and styles
 
+ public static Color menuAcceleratorForeground(boolean selection) {
+  Color color =
+   UIManager.getColor(selection ?
+    "MenuItem.acceleratorSelectionForeground" :
+    "MenuItem.acceleratorForeground");
+
+  if (color == null) color = defaultFgColor();
+
+  return color;
+ }
+
+ public static boolean isDarkLaf()
+ {
+  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.
@@ -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)
@@ -1471,7 +1530,7 @@
      comp = real;
    }
 
-   if(comp.getClass().equals(clazz))
+   if(clazz.isInstance(comp))
     return comp;
    else if(comp instanceof JPopupMenu)
     comp = ((JPopupMenu)comp).getInvoker();
@@ -1596,7 +1655,7 @@
   deprecatedIcons.put("NextFile.png",    "22x22/go-last.png");
   deprecatedIcons.put("PreviousFile.png","22x22/go-first.png");
 
-  deprecatedIcons.put("closebox.gif",   "10x10/actions/close.png");
+  deprecatedIcons.put("closebox.gif",   "32x32/actions/process-stop.svg?scale=0.33");
   deprecatedIcons.put("normal.gif",   "10x10/status/document-unmodified.png");
   deprecatedIcons.put("readonly.gif",   "10x10/emblem/emblem-readonly.png");
   deprecatedIcons.put("dirty.gif",    "10x10/status/document-modified.png");
@@ -1619,6 +1678,21 @@
  }
  //}}}
 
+ //{{{ isPopupTrigger() method
+ /**
+  * Returns if the specified event is the popup trigger event.
+  * This implements precisely defined behavior, as opposed to
+  * MouseEvent.isPopupTrigger().
+  * @param evt The event
+  * @since jEdit 3.2pre8
+  * @deprecated use {@link GenericGUIUtilities#requestFocus(Window, Component)}
+  */
+ @Deprecated
+ public static boolean isPopupTrigger(MouseEvent evt)
+ {
+  return GenericGUIUtilities.isPopupTrigger(evt);
+ } //}}}
+
  //{{{ init() method
  static void init()
  {
diff -ru jedit5.7.0/jEdit/build.xml jedit5.7.0-patched/jEdit/build.xml
--- jedit5.7.0/jEdit/build.xml 2024-08-03 19:53:28.000000000 +0200
+++ jedit5.7.0-patched/jEdit/build.xml 2025-04-16 17:20:57.401732024 +0200
@@ -488,6 +488,7 @@
     <include name="org/gjt/sp/jedit/icons/**/*.gif"/>
     <include name="org/gjt/sp/jedit/icons/**/*.jpg"/>
     <include name="org/gjt/sp/jedit/icons/**/*.png"/>
+    <include name="org/gjt/sp/jedit/icons/**/*.svg"/>
     <include name="org/jedit/localization/*.props"/>
    </fileset>
   </jar>
@@ -783,6 +784,7 @@
     <include name="*.txt"/>
     <include name="*.html"/>
     <include name="*.png"/>
+    <include name="*.svg"/>
     <include name="tips/**"/>
    </fileset>
   </copy>
diff -ru jedit5.7.0/jEdit/ivy.xml jedit5.7.0-patched/jEdit/ivy.xml
--- jedit5.7.0/jEdit/ivy.xml 2024-08-03 19:53:28.000000000 +0200
+++ jedit5.7.0-patched/jEdit/ivy.xml 2025-04-16 12:22:57.782535840 +0200
@@ -94,5 +94,8 @@
   <dependency org="com.google.code.findbugs" name="jsr305" rev="3.0.2"/>
 
   <dependency org="com.evolvedbinary.appbundler" name="appbundler" rev="1.3.0" conf="appbundler"/>
+
+  <dependency org="com.formdev" name="flatlaf" rev="3.6"/>
+  <dependency org="com.formdev" name="flatlaf-extras" rev="3.6"/>
  </dependencies>
 </ivy-module>
diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/MarkerViewer.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/MarkerViewer.java
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/MarkerViewer.java 2024-08-03 19:53:18.000000000 +0200
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/MarkerViewer.java 2025-04-16 21:35:23.519418287 +0200
@@ -50,28 +50,28 @@
   toolBar.add(Box.createGlue());
 
   RolloverButton addMarker = new RolloverButton(
-   GUIUtilities.loadIcon("Plus.png"));
+   GUIUtilities.loadIcon(jEdit.getProperty("add-marker.icon.small")));
   addMarker.setToolTipText(GenericGUIUtilities.prettifyMenuLabel(
    jEdit.getProperty("add-marker.label")));
   addMarker.addActionListener(this);
   addMarker.setActionCommand("add-marker");
   toolBar.add(addMarker);
 
-  previous = new RolloverButton(GUIUtilities.loadIcon("ArrowL.png"));
+  previous = new RolloverButton(GUIUtilities.loadIcon(jEdit.getProperty("prev-marker.icon.small")));
   previous.setToolTipText(GenericGUIUtilities.prettifyMenuLabel(
    jEdit.getProperty("prev-marker.label")));
   previous.addActionListener(this);
   previous.setActionCommand("prev-marker");
   toolBar.add(previous);
 
-  next = new RolloverButton(GUIUtilities.loadIcon("ArrowR.png"));
+  next = new RolloverButton(GUIUtilities.loadIcon(jEdit.getProperty("next-marker.icon.small")));
   next.setToolTipText(GenericGUIUtilities.prettifyMenuLabel(
    jEdit.getProperty("next-marker.label")));
   next.addActionListener(this);
   next.setActionCommand("next-marker");
   toolBar.add(next);
 
-  clear = new RolloverButton(GUIUtilities.loadIcon("Clear.png"));
+  clear = new RolloverButton(GUIUtilities.loadIcon(jEdit.getProperty("remove-all-markers.icon.small")));
   clear.setToolTipText(GenericGUIUtilities.prettifyMenuLabel(
    jEdit.getProperty("remove-all-markers.label")));
   clear.addActionListener(this);
diff -Nru jedit5.7.0/jEdit/org/gjt/sp/jedit/jedit_gui.props jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/jedit_gui.props
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/jedit_gui.props 2024-08-03 19:53:20.000000000 +0200
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/jedit_gui.props 2025-08-23 18:50:05.907962159 +0200
@@ -8,13 +8,15 @@
 ##java.lang.NullPointerException
 
 #{{{ Common icons
-common.add.icon=22x22/actions/list-add.png
-common.remove.icon=22x22/actions/list-remove.png
-common.moveUp.icon=22x22/actions/go-up.png
-common.moveDown.icon=22x22/actions/go-down.png
-common.clearAll.icon=22x22/actions/edit-clear.png
+common.add.icon=32x32/actions/list-add.svg?scale=0.7
+common.remove.icon=32x32/actions/list-remove.svg?scale=0.7
+common.moveUp.icon=32x32/actions/go-up.svg?scale=0.7
+common.moveDown.icon=32x32/actions/go-down.svg?scale=0.7
+common.clearAll.icon=32x32/actions/edit-clear.svg?scale=0.7
 logo.icon.small=16x16/apps/jedit.png
 logo.icon.medium=32x32/apps/jedit.png
+navigate-backwards.icon=idea-icons/expui/general/chevronLeft.svg?scale=1.2
+navigate-forwards.icon=idea-icons/expui/general/chevronRight.svg?scale=1.2
 
 #}}}
 
@@ -28,8 +30,8 @@
 defer=false
 startup=true
 
-broken-image.icon=22x22/status/image-missing.png
-dropdown-arrow.icon=ToolbarMenu.gif
+broken-image.icon=32x32/status/image-missing.svg?scale=0.7
+dropdown-arrow.icon=idea-icons/general/buttonDropTriangle.svg
 #}}}
 
 #{{{ Tool bar
@@ -39,68 +41,69 @@
  buffer-options combined-options - \
  plugin-manager - help
 
-new-file.icon=22x22/actions/document-new.png
-open-file.icon=22x22/actions/document-open.png
-save.icon=22x22/actions/document-save.png
-close-buffer.icon=22x22/actions/document-close.png
-global-close-buffer.icon=22x22/actions/document-close.png
-print.icon=22x22/actions/document-print.png
+new-file.icon=32x32/actions/document-new.svg?scale=0.7
+open-file.icon=32x32/actions/document-open.svg?scale=0.7
+save.icon=32x32/actions/document-save.svg?scale=0.7
+close-buffer.icon=32x32/actions/process-stop.svg?scale=0.7
+global-close-buffer.icon=32x32/actions/process-stop.svg?scale=0.7
+print.icon=32x32/actions/document-print.svg?scale=0.7
 page-setup.icon=22x22/actions/printer-setup.png
-undo.icon=22x22/actions/edit-undo.png
-redo.icon=22x22/actions/edit-redo.png
-cut.icon=22x22/actions/edit-cut.png
-copy.icon=22x22/actions/edit-copy.png
-paste.icon=22x22/actions/edit-paste.png
-find.icon=22x22/actions/edit-find.png
-find-next.icon=22x22/actions/edit-find-next.png
-new-view.icon=22x22/actions/window-new.png
+undo.icon=32x32/actions/edit-undo.svg?scale=0.7
+redo.icon=32x32/actions/edit-redo.svg?scale=0.7
+cut.icon=32x32/actions/edit-cut.svg?scale=0.7
+copy.icon=32x32/actions/edit-copy.svg?scale=0.7
+paste.icon=32x32/actions/edit-paste.svg?scale=0.7
+find.icon=32x32/actions/edit-find.svg?scale=0.7
+find-prev.icon=32x32/actions/go-previous.svg?scale=0.7
+find-next.icon=32x32/actions/go-next.svg?scale=0.7
+new-view.icon=32x32/actions/window-new.svg?scale=0.7
 unsplit.icon=22x22/actions/window-unsplit.png
 split-horizontal.icon=22x22/actions/window-split-horizontal.png
 split-vertical.icon=22x22/actions/window-split-vertical.png
-buffer-options.icon=22x22/actions/document-properties.png
-global-options.icon=22x22/categories/preferences-system.png
-combined-options.icon=22x22/categories/preferences-system.png
+buffer-options.icon=32x32/actions/document-properties.svg?scale=0.7
+global-options.icon=32x32/categories/preferences-system.svg?scale=0.7
+combined-options.icon=32x32/categories/preferences-system.svg?scale=0.7
 plugin-manager.icon=22x22/places/plugins.png
-help.icon=22x22/apps/help-browser.png
+help.icon=22x22/apps/help-browser.svg
 
 #{{{ Icon list for tool bar editor
 icons=22x22/actions/resize-horisontal.png \
- 22x22/actions/go-down.png \
- 22x22/actions/go-previous.png \
- 22x22/actions/go-next.png \
- 22x22/actions/go-home.png \
- 22x22/actions/go-up.png \
- 22x22/actions/go-first.png \
- 22x22/actions/go-last.png \
- 22x22/actions/go-parent.png \
- 22x22/actions/document-close.png \
- 22x22/actions/edit-undo.png \
- 22x22/actions/edit-redo.png \
- 22x22/actions/edit-cut.png \
- 22x22/actions/edit-paste.png \
- 22x22/actions/edit-delete.png \
- 22x22/actions/edit-clear.png \
- 22x22/actions/edit-find-next.png \
- 22x22/actions/edit-find-in-folder.png \
- 22x22/actions/edit-find.png \
- 22x22/actions/edit-copy.png \
+ 22x22/actions/go-down.svg \
+ 22x22/actions/go-previous.svg \
+ 22x22/actions/go-next.svg \
+ 32x32/actions/go-home.svg?scale=0.7 \
+ 22x22/actions/go-up.svg \
+ 22x22/actions/go-first.svg \
+ 22x22/actions/go-last.svg \
+ 22x22/actions/go-up.svg \
+ 32x32/actions/process-stop.svg?scale=0.7 \
+ 32x32/actions/edit-undo.svg?scale=0.7 \
+ 32x32/actions/edit-redo.svg?scale=0.7 \
+ 32x32/actions/edit-cut.svg?scale=0.7 \
+ 32x32/actions/edit-paste.svg?scale=0.7 \
+ scalable/actions/edit-delete.svg \
+ 22x22/actions/edit-clear.svg \
+ 22x22/actions/go-next.svg \
+ 32x32/actions/system-search.svg?scale=0.7 \
+ 32x32/actions/edit-find.svg?scale=0.7 \
+ 32x32/actions/edit-copy.svg?scale=0.7 \
  22x22/actions/copy-to-buffer.png \
- 22x22/actions/list-remove.png \
- 22x22/actions/list-add.png \
- 22x22/actions/folder-new.png \
- 22x22/actions/window-new.png \
- 22x22/actions/document-new.png \
- 22x22/actions/document-open.png \
+ 32x32/actions/list-remove.svg?scale=0.7 \
+ 32x32/actions/list-add.svg?scale=0.7 \
+ 32x32/actions/folder-new.svg?scale=0.7 \
+ 32x32/actions/document-new.svg?scale=0.7 \
+ 32x32/actions/document-new.svg?scale=0.7 \
+ 32x32/actions/document-open.svg?scale=0.7 \
  22x22/actions/document-reload2.png \
- 22x22/actions/document-properties.png \
- 22x22/actions/document-save.png \
- 22x22/actions/document-save-all.png \
- 22x22/actions/document-save-as.png \
+ 32x32/actions/document-properties.svg?scale=0.7 \
+ 32x32/actions/document-save.svg?scale=0.7 \
+ 32x32/actions/document-save-all.svg?scale=0.5 \
+ 32x32/actions/document-save-as.svg?scale=0.7 \
  22x22/actions/printer-setup.png \
- 22x22/actions/process-stop.png \
- 22x22/actions/media-playback-pause.png \
- 22x22/actions/media-playback-start.png \
- 22x22/actions/view-refresh.png \
+ 22x22/actions/system-log-out.svg \
+ 22x22/actions/media-playback-pause.svg \
+ 22x22/actions/media-playback-start.svg \
+ 22x22/actions/view-refresh.svg \
  22x22/actions/application-run.png \
  22x22/actions/edit-find-multiple.png \
  22x22/actions/edit-find-single.png \
@@ -109,18 +112,18 @@
  22x22/actions/window-unsplit.png \
  22x22/actions/zoom-in.png \
  22x22/actions/zoom-out.png \
- 22x22/apps/utilities-terminal.png \
- 22x22/apps/system-file-manager.png \
- 22x22/apps/internet-web-browser.png \
- 22x22/apps/help-browser.png \
- 22x22/apps/system-installer.png \
- 22x22/status/image-missing.png \
- 22x22/status/folder-visiting.png \
- 22x22/devices/drive-harddisk.png \
- 22x22/devices/media-floppy.png \
- 22x22/devices/printer.png \
+ 22x22/apps/utilities-terminal.svg \
+ 32x32/apps/system-file-manager.svg?scale=0.7 \
+ 32x32/apps/internet-web-browser.svg?scale=0.7 \
+ 22x22/apps/help-browser.svg \
+ 32x32/apps/system-installer.svg?scale=0.7 \
+ 32x32/status/image-missing.svg?scale=0.7 \
+ 32x32/status/folder-visiting.svg?scale=0.7 \
+ 32x32/devices/drive-harddisk.svg?scale=0.7 \
+ 22x22/devices/media-floppy.svg \
+ 32x32/devices/printer.svg?scale=0.7 \
  22x22/places/plugins.png \
- 22x22/categories/preferences-system.png \
+ 32x32/categories/preferences-system.svg?scale=0.7 \
  Blank24.gif
 #}}}
 
@@ -144,6 +147,7 @@
   new-file-in-mode \
   open-file \
   %recent-files \
+  %recent-directories \
   - \
   reload \
   reload-all \
@@ -163,31 +167,31 @@
   print \
   - \
   exit
-new-file.icon.small=16x16/actions/document-new.png
-new-file-in-mode.icon.small=16x16/actions/document-new.png
-open-file.icon.small=16x16/actions/document-open.png
-reload.icon.small=16x16/actions/view-refresh.png
-reload-all.icon.small=16x16/actions/view-refresh.png
-close-buffer.icon.small=16x16/actions/document-close.png
-closeall-bufferset.icon.small=16x16/actions/document-close.png
-closeall-except-active.icon.small=16x16/actions/document-close.png
-global-close-buffer.icon.small=16x16/actions/document-close.png
-close-all.icon.small=16x16/actions/document-close.png
-save.icon.small=16x16/actions/document-save.png
-save-as.icon.small=16x16/actions/document-save-as.png
-save-a-copy-as.icon.small=16x16/actions/document-save-as.png
-save-all.icon.small=16x16/actions/document-save-all.png
-print.icon.small=16x16/actions/document-print.png
-page-setup.icon.small=16x16/actions/document-properties.png
-exit.icon.small=16x16/actions/process-stop.png
-exit.icon.medium=22x22/actions/process-stop.png
+new-file.icon.small=32x32/actions/document-new.svg?scale=0.5
+new-file-in-mode.icon.small=32x32/actions/document-new.svg?scale=0.5
+open-file.icon.small=32x32/actions/document-open.svg?scale=0.5
+reload.icon.small=16x16/actions/view-refresh.svg
+reload-all.icon.small=16x16/actions/view-refresh.svg
+close-buffer.icon.small=32x32/actions/process-stop.svg?scale=0.5
+closeall-bufferset.icon.small=32x32/actions/process-stop.svg?scale=0.5
+closeall-except-active.icon.small=32x32/actions/process-stop.svg?scale=0.5
+global-close-buffer.icon.small=32x32/actions/process-stop.svg?scale=0.5
+close-all.icon.small=32x32/actions/process-stop.svg?scale=0.5
+save.icon.small=32x32/actions/document-save.svg?scale=0.5
+save-as.icon.small=32x32/actions/document-save-as.svg?scale=0.5
+save-a-copy-as.icon.small=32x32/actions/document-save-as.svg?scale=0.5
+save-all.icon.small=32x32/actions/document-save.svg?scale=0.5
+print.icon.small=32x32/actions/document-print.svg?scale=0.5
+page-setup.icon.small=32x32/actions/document-properties.svg?scale=0.5
+exit.icon.small=16x16/actions/system-log-out.svg
+exit.icon.medium=22x22/actions/system-log-out.svg
 
 #{{{ Recent Files menu
 recent-files.code=new RecentFilesProvider();
 #}}}
 
 reload-encoding.code=new ReloadWithEncodingProvider();
-reload-encoding.icon.small=16x16/actions/view-refresh.png
+reload-encoding.icon.small=16x16/actions/view-refresh.svg
 #}}}
 
 #{{{ Edit menu
@@ -211,12 +215,12 @@
   %text \
   %indent \
   %source
-undo.icon.small=16x16/actions/edit-undo.png
-redo.icon.small=16x16/actions/edit-redo.png
-cut.icon.small=16x16/actions/edit-cut.png
-copy.icon.small=16x16/actions/edit-copy.png
-paste.icon.small=16x16/actions/edit-paste.png
-select-all.icon.small=16x16/actions/edit-select-all.png
+undo.icon.small=32x32/actions/edit-undo.svg?scale=0.5
+redo.icon.small=32x32/actions/edit-redo.svg?scale=0.5
+cut.icon.small=32x32/actions/edit-cut.svg?scale=0.5
+copy.icon.small=32x32/actions/edit-copy.svg?scale=0.5
+paste.icon.small=32x32/actions/edit-paste.svg?scale=0.5
+select-all.icon.small=16x16/actions/edit-select-all.svg
 
 #{{{ More Clipboard menu
 clipboard=cut-append \
@@ -308,16 +312,18 @@
     regexp \
     - \
     hypersearch-results
-find.icon.small=22x22/actions/edit-find.png
-find-next.icon.small=22x22/actions/edit-find-next.png
-search-in-directory.icon.small=22x22/actions/edit-find-in-folder.png
-replace-in-selection.icon.small=22x22/actions/edit-find-replace.png
-replace-and-find-next.icon.small=22x22/actions/edit-find-replace.png
-replace-all.icon.small=22x22/actions/edit-find-replace.png
-quick-search.icon.small=22x22/actions/edit-find.png
-hypersearch.icon.small=22x22/actions/edit-find-multiple.png
-quick-search-word.icon.small=22x22/actions/edit-find.png
-hypersearch-word.icon.small=22x22/actions/edit-find.png
+find.icon.small=32x32/actions/edit-find.svg?scale=0.7
+find-prev.icon.small=32x32/actions/go-previous.svg?scale=0.7
+find-next.icon.small=32x32/actions/go-next.svg?scale=0.7
+search-in-open-buffers.icon.small=32x32/actions/system-search.svg?scale=0.7
+search-in-directory.icon.small=32x32/actions/system-search.svg?scale=0.7
+replace-in-selection.icon.small=32x32/actions/edit-find-replace.svg?scale=0.7
+replace-and-find-next.icon.small=32x32/actions/edit-find-replace.svg?scale=0.7
+replace-all.icon.small=32x32/actions/edit-find-replace.svg?scale=0.7
+quick-search.icon.small=32x32/actions/edit-find.svg?scale=0.7
+hypersearch.icon.small=32x32/actions/edit-find.svg?scale=0.7
+quick-search-word.icon.small=32x32/actions/edit-find.svg?scale=0.7
+hypersearch-word.icon.small=32x32/actions/edit-find.svg?scale=0.7
 #}}}
 
 #{{{ Markers menu
@@ -336,12 +342,12 @@
    view-markers \
    -
 markers.code=new MarkersProvider();
-add-marker.icon.small=22x22/actions/bookmark-new.png
-add-marker-shortcut.icon.small=22x22/actions/bookmark-new.png
-remove-all-markers.icon.small=22x22/actions/edit-clear.png
-goto-marker.icon.small=22x22/actions/go-jump.png
-prev-marker.icon.small=22x22/actions/go-previous.png
-next-marker.icon.small=22x22/actions/go-next.png
+add-marker.icon.small=32x32/actions/bookmark-new.svg?scale=0.7
+add-marker-shortcut.icon.small=32x32/actions/bookmark-new.svg?scale=0.7
+remove-all-markers.icon.small=32x32/actions/edit-clear.svg?scale=0.7
+goto-marker.icon.small=32x32/actions/go-jump.svg?scale=0.7
+prev-marker.icon.small=32x32/actions/go-previous.svg?scale=0.7
+next-marker.icon.small=32x32/actions/go-next.svg?scale=0.7
 #}}}
 
 #{{{ Folding menu
@@ -388,9 +394,12 @@
   - \
   set-view-title \
   toggle-full-screen
-new-view.icon.small=16x16/actions/window-new.png
-new-plain-view.icon.small=16x16/actions/window-new.png
-close-view.icon.small=16x16/actions/document-close.png
+new-view.icon.small=32x32/actions/window-new.svg?scale=0.5
+new-plain-view.icon.small=32x32/actions/window-new.svg?scale=0.5
+close-view.icon.small=32x32/actions/process-stop.svg?scale=0.5
+prev-buffer.icon.small=32x32/actions/go-previous.svg?scale=0.5
+next-buffer.icon.small=32x32/actions/go-next.svg?scale=0.5
+recent-buffer.icon.small=32x32/actions/go-up.svg?scale=0.5
 
 #{{{ Scrolling menu
 scrolling=scroll-to-current-line \
@@ -436,7 +445,6 @@
 
 #{{{ Utilities menu
 utils=vfs.browser \
-   %recent-directories \
    - \
    %favorites \
    %current-directory \
@@ -454,9 +462,9 @@
    - \
    %quick-options
 
-buffer-options.icon.small=16x16/actions/document-properties.png
-global-options.icon.small=16x16/categories/preferences-system.png
-combined-options.icon.small=16x16/categories/preferences-system.png
+buffer-options.icon.small=32x32/actions/document-properties.svg?scale=0.5
+global-options.icon.small=32x32/categories/preferences-system.svg?scale=0.5
+combined-options.icon.small=32x32/categories/preferences-system.svg?scale=0.5
 
 #{{{ Recent Directories menu
 recent-directories.code=new RecentDirectoriesProvider();
@@ -518,9 +526,9 @@
     rescan-macros \
     -
 macros.code=new MacrosProvider();
-new-macro.icon.small=16x16/actions/document-new.png
-record-macro.icon.small=16x16/actions/media-record.png
-stop-recording.icon.small=16x16/actions/media-playback-stop.png
+new-macro.icon.small=32x32/actions/document-new.svg?scale=0.5
+record-macro.icon.small=16x16/actions/media-record.svg
+stop-recording.icon.small=32x32/actions/media-playback-stop.svg?scale=0.5
 #}}}
 
 #{{{ Plugins menu
@@ -771,7 +779,7 @@
 
 #{{{ HyperSearch results dialog
 hypersearch-results.clear.icon=22x22/actions/edit-clear.png
-hypersearch-results.stop.icon=22x22/actions/process-stop.png
+hypersearch-results.stop.icon=22x22/actions/system-log-out.png
 hypersearch-results.multi.multiple.icon=22x22/actions/edit-find-multiple.png
 hypersearch-results.multi.single.icon=22x22/actions/edit-find-single.png
 hypersearch-results.match.highlight.icon=22x22/actions/edit-find-highlight-match.png
@@ -784,8 +792,8 @@
 #}}}
 
 #{{{ Help Viewer
-helpviewer.back.icon=22x22/actions/go-previous.png
-helpviewer.forward.icon=22x22/actions/go-next.png
+helpviewer.back.icon=32x32/actions/go-previous.svg?scale=0.7
+helpviewer.forward.icon=32x32/actions/go-next.svg?scale=0.7
 #}}}
 
 #}}}
@@ -809,9 +817,9 @@
 
 #{{{ Abbreviations pane
 options.abbrevs.code=new AbbrevsOptionPane();
-options.abbrevs.add.icon=22x22/actions/list-add.png
-options.abbrevs.edit.icon=22x22/actions/document-properties.png
-options.abbrevs.remove.icon=22x22/actions/list-remove.png
+options.abbrevs.add.icon=32x32/actions/list-add.svg?scale=0.7
+options.abbrevs.edit.icon=32x32/actions/document-properties.svg?scale=0.7
+options.abbrevs.remove.icon=32x32/actions/list-remove.svg?scale=0.7
 #}}}
 
 #{{{ Appearance pane
@@ -840,11 +848,11 @@
 
 #{{{ Context Menu pane
 options.context.code=new ContextOptionPane();
-options.context.add.icon=22x22/actions/list-add.png
-options.context.remove.icon=22x22/actions/list-remove.png
-options.context.moveUp.icon=22x22/actions/go-up.png
-options.context.moveDown.icon=22x22/actions/go-down.png
-options.context.reset.icon=22x22/actions/edit-clear.png
+options.context.add.icon=32x32/actions/list-add.svg?scale=0.7
+options.context.remove.icon=32x32/actions/list-remove.svg?scale=0.7
+options.context.moveUp.icon=32x32/actions/go-up.svg?scale=0.7
+options.context.moveDown.icon=32x32/actions/go-down.svg?scale=0.7
+options.context.reset.icon=32x32/actions/edit-clear.svg?scale=0.7
 options.context.includeOptionsLink=true
 #}}}
 
@@ -906,12 +914,12 @@
 
 #{{{ Tool Bar pane
 options.toolbar.code=new ToolBarOptionPane();
-options.toolbar.add.icon=22x22/actions/list-add.png
-options.toolbar.remove.icon=22x22/actions/list-remove.png
-options.toolbar.moveUp.icon=22x22/actions/go-up.png
-options.toolbar.moveDown.icon=22x22/actions/go-down.png
-options.toolbar.reset.icon=22x22/actions/edit-clear.png
-options.toolbar.edit.icon=22x22/actions/document-properties.png
+options.toolbar.add.icon=32x32/actions/list-add.svg?scale=0.7
+options.toolbar.remove.icon=32x32/actions/list-remove.svg?scale=0.7
+options.toolbar.moveUp.icon=22x22/actions/go-up.svg
+options.toolbar.moveDown.icon=22x22/actions/go-down.svg
+options.toolbar.reset.icon=22x22/actions/edit-clear.svg
+options.toolbar.edit.icon=32x32/actions/document-properties.svg?scale=0.7
 #}}}
 
 #{{{ View pane
@@ -949,7 +957,8 @@
 vfs.browser.default-filter=*[^~#]
 vfs.browser.filter-enabled=true
 vfs.browser.file.icon=16x16/mimetypes/text-x-generic.png
-vfs.browser.icon.small=16x16/apps/system-file-manager.png
+vfs.browser.icon=32x32/apps/system-file-manager.svg?scale=0.7
+vfs.browser.icon.small=32x32/apps/system-file-manager.svg?scale=0.5
 vfs.browser.open-file.icon=16x16/actions/edit-select-all.png
 vfs.browser.dir.icon=16x16/places/folder.png
 vfs.browser.open-dir.icon=16x16/status/folder-open.png
@@ -1007,13 +1016,13 @@
 plugin-manager.mirror-url=http://plugins.jedit.org/export/mirror_list.php
 
 #{{{ Plugin management
-manage-plugins.restore.icon=22x22/actions/document-open.png
-manage-plugins.save.icon=22x22/actions/document-save.png
+manage-plugins.restore.icon=32x32/actions/document-open.svg?scale=0.7
+manage-plugins.save.icon=32x32/actions/document-save.svg?scale=0.7
 #}}}
 
 #{{{ Plugin installation
-install-plugins.choose-plugin-set.icon=22x22/actions/document-open.png
-install-plugins.clear-plugin-set.icon=22x22/actions/edit-clear.png
+install-plugins.choose-plugin-set.icon=32x32/actions/document-open.svg?scale=0.7
+install-plugins.clear-plugin-set.icon=22x22/actions/edit-clear.svg
 #}}}
 
 #}}}
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-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));
   ActionListener actionHandler = new ActionHandler();
-  JButton add = new RolloverButton(GUIUtilities.loadIcon("Plus.png"));
+  JButton add = new RolloverButton(GUIUtilities.loadIcon(jEdit.getProperty("common.add.icon")));
   add.setToolTipText(jEdit.getProperty("common.add"));
   add.addActionListener(e -> colorsModel.add());
   buttons.add(add);
   buttons.add(Box.createHorizontalStrut(6));
-  remove = new RolloverButton(GUIUtilities.loadIcon("Minus.png"));
+  remove = new RolloverButton(GUIUtilities.loadIcon(jEdit.getProperty("common.remove.icon")));
   remove.setToolTipText(jEdit.getProperty("common.remove"));
   remove.addActionListener(e ->
   {
@@ -93,12 +93,12 @@
   });
   buttons.add(remove);
   buttons.add(Box.createHorizontalStrut(6));
-  moveUp = new RolloverButton(GUIUtilities.loadIcon("ArrowU.png"));
+  moveUp = new RolloverButton(GUIUtilities.loadIcon(jEdit.getProperty("common.moveUp.icon")));
   moveUp.setToolTipText(jEdit.getProperty("common.moveUp"));
   moveUp.addActionListener(actionHandler);
   buttons.add(moveUp);
   buttons.add(Box.createHorizontalStrut(6));
-  moveDown = new RolloverButton(GUIUtilities.loadIcon("ArrowD.png"));
+  moveDown = new RolloverButton(GUIUtilities.loadIcon(jEdit.getProperty("common.moveDown.icon")));
   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
@@ -160,12 +160,12 @@
   buttons.setBorder(new EmptyBorder(3,0,0,0));
   buttons.setLayout(new BoxLayout(buttons,BoxLayout.X_AXIS));
   buttons.add(Box.createHorizontalStrut(6));
-  moveUp = new RolloverButton(GUIUtilities.loadIcon("ArrowU.png"));
+  moveUp = new RolloverButton(GUIUtilities.loadIcon(jEdit.getProperty("common.moveUp.icon")));
   moveUp.setToolTipText(jEdit.getProperty("options.status.moveUp"));
   moveUp.addActionListener(e -> moveUp());
   buttons.add(moveUp);
   buttons.add(Box.createHorizontalStrut(6));
-  moveDown = new RolloverButton(GUIUtilities.loadIcon("ArrowD.png"));
+  moveDown = new RolloverButton(GUIUtilities.loadIcon(jEdit.getProperty("common.moveDown.icon")));
   moveDown.setToolTipText(jEdit.getProperty("options.status.moveDown"));
   moveDown.addActionListener(e -> moveDown());
   buttons.add(moveDown);
diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/RegisterViewer.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/RegisterViewer.java
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/RegisterViewer.java 2024-08-03 19:53:18.000000000 +0200
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/RegisterViewer.java 2025-04-16 21:45:44.861713409 +0200
@@ -54,7 +54,7 @@
   toolBar.add(Box.createGlue());
 
   RolloverButton pasteRegister = new RolloverButton(
-   GUIUtilities.loadIcon("Paste.png"));
+   GUIUtilities.loadIcon(jEdit.getProperty("paste.icon")));
   pasteRegister.setToolTipText(GenericGUIUtilities.prettifyMenuLabel(
    jEdit.getProperty("paste-string-register.label")));
   pasteRegister.addActionListener(e -> insertRegister());
@@ -62,7 +62,7 @@
   toolBar.add(pasteRegister);
 
   RolloverButton clearRegister = new RolloverButton(
-   GUIUtilities.loadIcon("Clear.png"));
+   GUIUtilities.loadIcon(jEdit.getProperty("common.clearAll.icon")));
   clearRegister.setToolTipText(GenericGUIUtilities.prettifyMenuLabel(
    jEdit.getProperty("clear-string-register.label")));
   clearRegister.addActionListener(e -> clearSelectedIndex());
diff -Nru 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-08-23 12:21:08.098088170 +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
@@ -2615,7 +2626,9 @@
     view.getEditPane().saveCaretInfo();
    }
 
-   View newView = new View(buffer,config);
+   ViewFactory viewFactory = ServiceManager.getService(ViewFactory.class, "view-factory");
+   View newView =
+    viewFactory == null ? new View(buffer,config) : viewFactory.create(buffer,config);
    viewManager.addViewToList(newView);
 
    EditBus.send(new ViewUpdate(newView,ViewUpdate.CREATED));
@@ -4233,7 +4246,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/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 -Nru 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-11-28 19:22:09.823220894 +0100
@@ -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;
@@ -50,11 +51,13 @@
 import org.gjt.sp.jedit.textarea.AntiAlias;
 import org.gjt.sp.jedit.textarea.Gutter;
 import org.gjt.sp.jedit.textarea.JEditTextArea;
+import org.gjt.sp.jedit.textarea.JEditTextAreaFactory;
 import org.gjt.sp.jedit.textarea.MouseHandler;
 import org.gjt.sp.jedit.textarea.Selection;
 import org.gjt.sp.jedit.textarea.StatusListener;
 import org.gjt.sp.jedit.textarea.TextArea;
 import org.gjt.sp.jedit.textarea.TextAreaExtension;
+import org.gjt.sp.jedit.textarea.TextAreaMouseHandler;
 import org.gjt.sp.jedit.textarea.TextAreaPainter;
 import org.gjt.sp.jedit.textarea.TextAreaTransferHandler;
 import org.gjt.sp.util.SyntaxUtilities;
@@ -380,9 +383,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;
@@ -756,7 +761,7 @@
  //{{{ Package-private members
 
  //{{{ EditPane constructor
- EditPane(@Nonnull View view, @Nullable BufferSet bufferSetSource, @Nonnull Buffer buffer)
+ public EditPane(@Nonnull View view, @Nullable BufferSet bufferSetSource, @Nonnull Buffer buffer)
  {
   super(new BorderLayout());
   BufferSet.Scope scope = jEdit.getBufferSetManager().getScope();
@@ -795,10 +800,17 @@
   this.view = view;
 
 
-  textArea = new JEditTextArea(view);
+  JEditTextAreaFactory textAreaFactory =
+   ServiceManager.getService(JEditTextAreaFactory.class, "textarea-factory");
+  textArea =
+   textAreaFactory == null ? new JEditTextArea(view) : textAreaFactory.create(view);
   bufferSet.addBufferSetListener(this);
   textArea.getPainter().setAntiAlias(new AntiAlias(jEdit.getProperty("view.antiAlias")));
-  textArea.setMouseHandler(new MouseHandler(textArea));
+  EditPaneMouseHandlerFactory mouseHandlerFactory =
+   ServiceManager.getService(EditPaneMouseHandlerFactory.class, "mouse-handler-factory");
+        TextAreaMouseHandler mouseHandler =
+         mouseHandlerFactory == null ? new MouseHandler(textArea) : mouseHandlerFactory.create(this);
+  textArea.setMouseHandler(mouseHandler);
   textArea.setTransferHandler(new TextAreaTransferHandler());
   markerHighlight = new MarkerHighlight();
   Gutter gutter = textArea.getGutter();
@@ -1029,7 +1041,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 -Nru jedit5.7.0/jEdit/org/gjt/sp/jedit/EditPaneMouseHandlerFactory.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/EditPaneMouseHandlerFactory.java
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/EditPaneMouseHandlerFactory.java 1970-01-01 01:00:00.000000000 +0100
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/EditPaneMouseHandlerFactory.java 2025-11-28 19:16:11.269418129 +0100
@@ -0,0 +1,14 @@
+package org.gjt.sp.jedit;
+
+import org.gjt.sp.jedit.textarea.JEditTextArea;
+import org.gjt.sp.jedit.textarea.TextAreaMouseHandler;
+import org.gjt.sp.jedit.textarea.MouseHandler;
+
+
+public class EditPaneMouseHandlerFactory
+{
+    public TextAreaMouseHandler create(EditPane editPane)
+    {
+        return new MouseHandler(editPane.getTextArea());
+    }
+}
diff -Nru jedit5.7.0/jEdit/org/gjt/sp/jedit/textarea/TextAreaMouseHandler.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextAreaMouseHandler.java
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/textarea/TextAreaMouseHandler.java 2024-08-03 19:53:18.000000000 +0200
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextAreaMouseHandler.java 2025-11-28 19:37:46.852139435 +0100
@@ -45,7 +45,7 @@
 public class TextAreaMouseHandler extends MouseInputAdapter
 {
  //{{{ MouseHandler constructor
- TextAreaMouseHandler(TextArea textArea)
+ protected TextAreaMouseHandler(TextArea textArea)
  {
   this.textArea = textArea;
  } //}}}
@@ -341,7 +341,7 @@
  } //}}}
 
  //{{{ doSingleDrag() method
- private void doSingleDrag(MouseEvent evt)
+ protected void doSingleDrag(MouseEvent evt)
  {
   dragged = true;
 
@@ -413,7 +413,7 @@
  } //}}}
 
  //{{{ doDoubleDrag() method
- private void doDoubleDrag(MouseEvent evt)
+ protected void doDoubleDrag(MouseEvent evt)
  {
   int markLineStart = textArea.getLineStartOffset(dragStartLine);
   int markLineLength = textArea.getLineLength(dragStartLine);
@@ -480,7 +480,7 @@
  } //}}}
 
  //{{{ doTripleDrag() method
- private void doTripleDrag(MouseEvent evt)
+ protected void doTripleDrag(MouseEvent evt)
  {
   TextAreaPainter painter = textArea.getPainter();
 
@@ -683,7 +683,7 @@
   * Dynamically get the "pivot" point associated with a current
   * selection.  See inline comments for details.
   */
- private int getSelectionPivotCaret()
+ protected int getSelectionPivotCaret()
  {
   int caret = textArea.caret;
 
@@ -713,7 +713,7 @@
  /*
   * See getSelectionPivotCaret for an explanation of this function
   */
- private int getSelectionPivotLine()
+ protected int getSelectionPivotLine()
  {
   int c  = textArea.caret;
   int cl = textArea.caretLine;
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 -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/help/HistoryButton.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/help/HistoryButton.java
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/help/HistoryButton.java 2024-08-03 19:53:20.000000000 +0200
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/help/HistoryButton.java 2025-05-20 15:21:59.692613480 +0200
@@ -61,7 +61,7 @@
       ? "helpviewer.back.label"
       : "helpviewer.forward.label"));
   Box box = new Box(BoxLayout.X_AXIS);
-  drop_button = new RolloverButton(GUIUtilities.loadIcon(jEdit.getProperty("dropdown-arrow.icon")));
+  drop_button = new RolloverButton(GUIUtilities.loadIcon(jEdit.getThemeProperty("dropdown-arrow.icon")));
   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
diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 2024-08-03 19:53:18.000000000 +0200
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 2025-05-20 15:21:47.892811800 +0200
@@ -45,14 +45,15 @@
  * @version $Id: FloatingWindowContainer.java 25333 2020-05-10 09:40:02Z kpouer $
  * @since jEdit 4.0pre1
  */
-public class FloatingWindowContainer extends JFrame implements DockableWindowContainer, PropertyChangeListener
-{
+public class FloatingWindowContainer extends JDialog implements DockableWindowContainer, PropertyChangeListener {
  private String dockableName;
 
  //{{{ FloatingWindowContainer constructor
  public FloatingWindowContainer(DockableWindowManagerImpl dockableWindowManager,
   boolean clone)
  {
+  super(dockableWindowManager.getView());
+
   this.dockableWindowManager = dockableWindowManager;
 
   dockableWindowManager.addPropertyChangeListener(this);
@@ -62,7 +63,7 @@
 
   Box caption = new Box(BoxLayout.X_AXIS);
   caption.add(menu = new RolloverButton(GUIUtilities
-   .loadIcon(jEdit.getProperty("dropdown-arrow.icon"))));
+   .loadIcon(jEdit.getThemeProperty("dropdown-arrow.icon"))));
   menu.addMouseListener(new MouseHandler());
   menu.setToolTipText(jEdit.getProperty("docking.menu.label"));
   Box separatorBox = new Box(BoxLayout.Y_AXIS);
@@ -87,7 +88,6 @@
   pack();
   Container parent = dockableWindowManager.getView();
   GUIUtilities.loadGeometry(this, parent, dockableName);
-  GUIUtilities.addSizeSaver(this, parent, dockableName);
   KeyListener listener = dockableWindowManager.closeListener(dockableName);
   addKeyListener(listener);
   getContentPane().addKeyListener(listener);
@@ -154,8 +154,11 @@
  @Override
  public void dispose()
  {
-  entry.container = null;
-  entry.win = null;
+  GUIUtilities.saveGeometry(this, dockableWindowManager.getView(), dockableName);
+  if (entry != null) {
+   entry.container = null;
+   entry.win = null;
+  }
   super.dispose();
  } //}}}
 
diff -Nru jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java 2024-08-03 19:53:16.000000000 +0200
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java 2025-08-23 19:56:33.392876293 +0200
@@ -53,11 +53,13 @@
 import javax.swing.JComponent;
 import javax.swing.JPanel;
 import javax.swing.JPopupMenu;
+import javax.swing.JMenuItem;
 import javax.swing.JToggleButton;
 import javax.swing.UIManager;
 import javax.swing.border.Border;
 import javax.swing.border.EmptyBorder;
 import javax.swing.plaf.metal.MetalLookAndFeel;
+import javax.accessibility.AccessibleContext;
 
 import org.gjt.sp.jedit.EditBus;
 import org.gjt.sp.jedit.GUIUtilities;
@@ -99,7 +101,7 @@
 
   closeBox.addActionListener(e -> show((DockableWindowManagerImpl.Entry)null));
 
-  menuBtn = new JButton(GUIUtilities.loadIcon(jEdit.getProperty("dropdown-arrow.icon")));
+  menuBtn = new JButton(GUIUtilities.loadIcon(jEdit.getThemeProperty("dropdown-arrow.icon")));
   menuBtn.setRequestFocusEnabled(false);
   menuBtn.setToolTipText(jEdit.getProperty("view.docking.menu-tooltip"));
   if(OperatingSystem.isMacOSLF())
@@ -164,11 +166,13 @@
   {
    button = new JToggleButton(); 
    button.setMargin(new Insets(1,1,1,1));
+            button.setFont(new JMenuItem().getFont());
   }
   GenericGUIUtilities.setButtonContentMargin(button, new Insets(6,6,6,6));
   button.setRequestFocusEnabled(false);
-  button.setIcon(new RotatedTextIcon(rotation,button.getFont(),
-   entry.shortTitle()));
+  String shortTitle = entry.shortTitle();
+  button.setIcon(new RotatedTextIcon(rotation,button.getFont(), shortTitle));
+  button.putClientProperty(AccessibleContext.ACCESSIBLE_NAME_PROPERTY, shortTitle);
   button.setActionCommand(entry.factory.name);
   button.addActionListener(new ActionHandler());
   button.addMouseListener(new MenuMouseHandler());
@@ -683,8 +687,6 @@
    renderHints = new RenderingHints(
     RenderingHints.KEY_ANTIALIASING,
     RenderingHints.VALUE_ANTIALIAS_ON);
-   renderHints.put(RenderingHints.KEY_FRACTIONALMETRICS,
-    RenderingHints.VALUE_FRACTIONALMETRICS_ON);
    renderHints.put(RenderingHints.KEY_RENDERING,
     RenderingHints.VALUE_RENDER_QUALITY);
   } //}}}
diff -Nru jedit5.7.0/jEdit/org/gjt/sp/jedit/browser/BrowserView.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/browser/BrowserView.java
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/browser/BrowserView.java 2024-08-03 19:53:15.000000000 +0200
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/browser/BrowserView.java 2025-08-25 21:14:57.442610750 +0200
@@ -26,6 +26,7 @@
 import javax.swing.border.EmptyBorder;
 import javax.swing.event.*;
 import javax.swing.*;
+import javax.accessibility.AccessibleContext;
 
 import static java.awt.event.InputEvent.*;
 import java.awt.event.*;
@@ -61,6 +62,7 @@
   parentDirectories = new ParentDirectoryList();
   parentDirectories.addKeyListener(keyListener);
   parentDirectories.setName("parent");
+  parentDirectories.putClientProperty(AccessibleContext.ACCESSIBLE_NAME_PROPERTY, "Directory hierarchy");
 
   parentDirectories.getSelectionModel().setSelectionMode(ListSelectionModel.SINGLE_SELECTION);
   parentDirectories.setCellRenderer(new ParentDirectoryRenderer());
@@ -74,6 +76,8 @@
   table.addMouseListener(new TableMouseHandler());
   table.addKeyListener(new TableKeyListener());
   table.setName("file");
+  table.putClientProperty(AccessibleContext.ACCESSIBLE_NAME_PROPERTY, "Directory entries");
+
   JScrollPane tableScroller = new JScrollPane(table);
   tableScroller.setMinimumSize(new Dimension(0,0));
   tableScroller.getViewport().setBackground(table.getBackground());
diff -Nru jedit5.7.0/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java 2024-08-03 19:53:15.000000000 +0200
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java 2025-08-25 21:24:39.620005049 +0200
@@ -30,6 +30,7 @@
 import javax.swing.border.EmptyBorder;
 import javax.swing.event.*;
 import javax.swing.*;
+import javax.accessibility.AccessibleContext;
 import java.awt.datatransfer.DataFlavor;
 import java.awt.datatransfer.Transferable;
 import java.awt.datatransfer.UnsupportedFlavorException;
@@ -222,7 +223,7 @@
   pathField.setInstantPopups(true);
   pathField.setEnterAddsToHistory(false);
   pathField.setSelectAllOnFocus(true);
-
+  label.setLabelFor(pathField);
 
   // because its preferred size can be quite wide, we
   // don't want it to make the browser way too big,
@@ -239,6 +240,7 @@
   pathAndFilterPanel.add(pathField);
 
   filterCheckbox = new JCheckBox(jEdit.getProperty("vfs.browser.filter"));
+  filterCheckbox.putClientProperty(AccessibleContext.ACCESSIBLE_NAME_PROPERTY, "Filter enabled");
   filterCheckbox.setMargin(new Insets(0,0,0,0));
 // filterCheckbox.setRequestFocusEnabled(false);
   filterCheckbox.setBorder(new EmptyBorder(0,0,0,12));
@@ -257,9 +259,11 @@
    pathAndFilterPanel.add(filterCheckbox);
   }
 
+  String filterTooltip = jEdit.getProperty("vfs.browser.filter") + " " + jEdit.getProperty("glob.tooltip");
   filterField = new JComboBox<>();
   filterEditor = new HistoryComboBoxEditor("vfs.browser.filter");
-  filterEditor.setToolTipText(jEdit.getProperty("glob.tooltip"));
+  filterEditor.putClientProperty(AccessibleContext.ACCESSIBLE_NAME_PROPERTY, filterTooltip);
+  filterEditor.setToolTipText(filterTooltip);
   filterEditor.setInstantPopups(true);
   filterEditor.setSelectAllOnFocus(true);
   filterEditor.addActionListener(actionHandler);
@@ -1195,6 +1199,7 @@
   VFSFile[] selectedFiles = browserView.getSelectedFiles();
 
   Buffer buffer = null;
+  String bufferMarker = null;
 
 check_selected:
   for (VFSFile file : selectedFiles)
@@ -1244,7 +1249,10 @@
     }
 
     if (_buffer != null)
+    {
      buffer = _buffer;
+     bufferMarker = file.getPathMarker();
+    }
    }
    // otherwise if a file is selected in OPEN_DIALOG or
    // SAVE_DIALOG mode, just let the listener(s)
@@ -1253,21 +1261,30 @@
 
   if(buffer != null)
   {
+   View gotoView = null;
+
    switch(mode)
    {
    case M_OPEN:
     view.setBuffer(buffer);
+    gotoView = view;
     break;
    case M_OPEN_NEW_VIEW:
-    jEdit.newView(view,buffer,false);
+    gotoView = jEdit.newView(view,buffer,false);
     break;
    case M_OPEN_NEW_PLAIN_VIEW:
-    jEdit.newView(view,buffer,true);
+    gotoView = jEdit.newView(view,buffer,true);
     break;
    case M_OPEN_NEW_SPLIT:
     view.splitHorizontally().setBuffer(buffer);
+    gotoView = view;
     break;
    }
+
+   if (gotoView != null && bufferMarker != null)
+   {
+    jEdit.gotoMarker(gotoView, buffer, bufferMarker);
+   }
   }
 
   Object[] listeners = listenerList.getListenerList();
@@ -1751,7 +1768,7 @@
   //{{{ MenuButton constructor
   MenuButton()
   {
-   setIcon(GUIUtilities.loadIcon(jEdit.getProperty("dropdown-arrow.icon")));
+   setIcon(GUIUtilities.loadIcon(jEdit.getThemeProperty("dropdown-arrow.icon")));
    setHorizontalTextPosition(SwingConstants.LEADING);
 
  // setRequestFocusEnabled(false);
diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/io/VFSFile.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/io/VFSFile.java
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/io/VFSFile.java 2024-08-03 19:53:14.000000000 +0200
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/io/VFSFile.java 2024-10-29 11:50:54.062016616 +0100
@@ -302,6 +302,12 @@
   }
  } //}}}
 
+ //{{{ getPathMarker() method (for jEdit.gotoMarker)
+ public String getPathMarker()
+ {
+  return null;
+ } //}}}
+
  //{{{ getPath() method
  public String getPath()
  {
diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/options/AppearanceOptionPane.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/options/AppearanceOptionPane.java
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/options/AppearanceOptionPane.java 2024-08-03 19:53:15.000000000 +0200
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/options/AppearanceOptionPane.java 2025-05-21 15:34:14.464265550 +0200
@@ -93,7 +93,7 @@
   /* Icon Theme */
   String[] themes = IconTheme.builtInNames();
   iconThemes = new JComboBox<String>(themes);
-  addComponent(jEdit.getProperty("options.appearance.iconTheme"), iconThemes);
+  //addComponent(jEdit.getProperty("options.appearance.iconTheme"), iconThemes);
   String oldTheme = IconTheme.get();
   for (int i=0; i<themes.length; ++i)
   {
@@ -414,7 +414,9 @@
 
   // adjust swing properties for button, menu, and label, and list and
   // textfield fonts
-  setFonts();
+  if (!jEdit.getProperty("lookAndFeel").startsWith("com.formdev.flatlaf.")) {
+   setFonts();
+  }
 
   // This is handled a little differently from other jEdit settings
   // as this flag needs to be known very early in the
diff -Nru jedit5.7.0/jEdit/org/gjt/sp/jedit/ViewFactory.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/ViewFactory.java
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/ViewFactory.java 1970-01-01 01:00:00.000000000 +0100
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/ViewFactory.java 2025-08-23 12:25:51.494671519 +0200
@@ -0,0 +1,9 @@
+package org.gjt.sp.jedit;
+
+public class ViewFactory
+{
+    public View create(Buffer buffer, View.ViewConfig config)
+    {
+        return new View(buffer, config);
+    }
+}
diff -Nru jedit5.7.0/jEdit/org/gjt/sp/jedit/View.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/View.java
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/View.java 2024-08-03 19:53:15.000000000 +0200
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/View.java 2025-08-23 13:08:26.323848617 +0200
@@ -1264,15 +1264,10 @@
 
   StringBuilder title = new StringBuilder();
 
-  /* On Mac OS X, apps are not supposed to show their name in the
- title bar. */
-  if(!OperatingSystem.isMacOS())
-  {
-   if (userTitle != null)
-    title.append(userTitle);
-   else
-    title.append(jEdit.getProperty("view.title"));
-  }
+  if (userTitle != null)
+   title.append(userTitle);
+  else
+   title.append(jEdit.getProperty("view.title"));
 
   for(int i = 0; i < buffers.size(); i++)
   {
@@ -1355,7 +1350,7 @@
  View next;
 
  //{{{ View constructor
- View(Buffer buffer, ViewConfig config)
+ public View(Buffer buffer, ViewConfig config)
  {
   fullScreenMode = false;
   menuBar = null;
@@ -2070,7 +2065,11 @@
 
  private EditPane createEditPane(@Nullable BufferSet bufferSetSource, @Nonnull Buffer buffer)
  {
-  EditPane editPane = new EditPane(this, bufferSetSource, buffer);
+  EditPaneFactory editPaneFactory =
+   ServiceManager.getService(EditPaneFactory.class, "editpane-factory");
+  EditPane editPane =
+   editPaneFactory == null ? new EditPane(this, bufferSetSource, buffer) :
+   editPaneFactory.create(this, bufferSetSource, buffer);
   JEditTextArea textArea = editPane.getTextArea();
   textArea.addFocusListener(new FocusHandler());
   textArea.addCaretListener(new CaretHandler());
diff -Nru jedit5.7.0/jEdit/org/gjt/sp/jedit/EditPaneFactory.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/EditPaneFactory.java
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/EditPaneFactory.java 1970-01-01 01:00:00.000000000 +0100
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/EditPaneFactory.java 2025-08-22 13:21:29.596599634 +0200
@@ -0,0 +1,11 @@
+package org.gjt.sp.jedit;
+
+import org.gjt.sp.jedit.bufferset.BufferSet;
+
+public class EditPaneFactory
+{
+    public EditPane create(View view, BufferSet bufferSetSource, Buffer buffer)
+    {
+        return new EditPane(view, bufferSetSource, buffer);
+    }
+}
diff -Nru jedit5.7.0/jEdit/org/gjt/sp/jedit/textarea/JEditTextAreaFactory.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/textarea/JEditTextAreaFactory.java
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/textarea/JEditTextAreaFactory.java 1970-01-01 01:00:00.000000000 +0100
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/textarea/JEditTextAreaFactory.java 2025-08-22 13:21:51.268384088 +0200
@@ -0,0 +1,11 @@
+package org.gjt.sp.jedit.textarea;
+
+import org.gjt.sp.jedit.View;
+
+public class JEditTextAreaFactory
+{
+    public JEditTextArea create(View view)
+    {
+        return new JEditTextArea(view);
+    }
+}
diff -Nru jedit5.7.0/jEdit/org/gjt/sp/jedit/menu/RecentFilesProvider.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/menu/RecentFilesProvider.java
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/menu/RecentFilesProvider.java 2024-08-03 19:53:18.000000000 +0200
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/menu/RecentFilesProvider.java 2025-08-23 18:40:22.465744832 +0200
@@ -86,7 +86,7 @@
   final JTextField text = new JTextField();
   text.setToolTipText(jEdit.getProperty("recent-files.textfield.tooltip") +
    ": " + jEdit.getProperty("glob.tooltip"));
-  menu.add(text);
+  // menu.add(text);
   text.addKeyListener(new KeyAdapter()
   {
    @Override
diff -Nru jedit5.7.0/jEdit/org/gjt/sp/jedit/textarea/InputMethodSupport.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/textarea/InputMethodSupport.java
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/textarea/InputMethodSupport.java 2024-08-03 19:53:18.000000000 +0200
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/textarea/InputMethodSupport.java 2025-11-27 22:40:40.136594077 +0100
@@ -141,6 +141,8 @@
     if (selectionStartLine == caretLine)
     {
      Point selection_start = owner.offsetToXY(selection_on_caret.getStart());
+     if (selection_start == null)
+      return getCaretRectangle(0, 0);
      return getCaretRectangle(selection_start.x, selection_start.y);
     }
     else