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-05-20 15:40:14.181962645 +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)
@@ -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 -ru 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-05-20 13:46:50.541586193 +0200
@@ -8,13 +8,15 @@
###
#{{{ 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
#}}}
@@ -163,31 +166,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 +214,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 +311,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 +341,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 +393,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 \
@@ -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 -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();
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 -ru 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-05-20 15:21:53.380719554 +0200
@@ -53,6 +53,7 @@
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;
@@ -99,7 +100,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,6 +165,7 @@
{
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);
@@ -683,8 +685,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 -ru 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-05-20 15:21:39.685949775 +0200
@@ -1195,6 +1195,7 @@
VFSFile[] selectedFiles = browserView.getSelectedFiles();
Buffer buffer = null;
+ String bufferMarker = null;
check_selected:
for (VFSFile file : selectedFiles)
@@ -1244,7 +1245,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 +1257,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 +1764,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