| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Tools/jEdit/patches/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 72 kB |
|
SSL main Sprache: unbekannt |
|
|
Quellsprache: Binärcode aufgebrochen in jeweils 16 ZeichenUnknown {[0] [0] [0]}zum Wurzelverzeichnis wechseln diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java jedit5.7.0-patched/jEd --- jedit5.7.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2024-08-03 19:53:18.0000000 +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2024-10-29 11:50:54 @@ -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 Gly + 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-patch --- jedit5.7.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2024-08-03 19:53:18.00 +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2025-08-24 16: @@ -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(thi 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 je --- jedit5.7.0/jEdit/org/gjt/sp/jedit/textarea/TextAreaPainterFactory.java 1970-01 +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextAreaPainterFactory.jav @@ -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. --- jedit5.7.0/jEdit/org/gjt/sp/jedit/textarea/TextAreaPainter.java 2024-08-03 19:5 +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextAreaPainter.java 2025-0 @@ -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/jE --- jedit5.7.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 2024-08-03 19:53:20.000000 +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/TextUtilities.java 2024-10-29 11:50:5 @@ -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/jE --- jedit5.7.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java 2024-08-03 19:53:15.0000000 +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/GUIUtilities.java 2025-08-23 15:00:39 @@ -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="ap + + <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 --- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/MarkerViewer.java 2024-08-03 19:53:18.000 +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/MarkerViewer.java 2025-04-16 21:3 @@ -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 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.ico 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-mar 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/jEdi --- jedit5.7.0/jEdit/org/gjt/sp/jedit/jedit_gui.props 2024-08-03 19:53:20.000000000 +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/jedit_gui.props 2025-08-23 18:50:05.9 @@ -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 #}}} @@ -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 @@ -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. +install-plugins.clear-plugin-set.icon=22x22/actions/edit-clear.svg #}}} #}}} diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/options/BrowserColorsOptionPane.java jed --- jedit5.7.0/jEdit/org/gjt/sp/jedit/options/BrowserColorsOptionPane.java 2024-08 +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/options/BrowserColorsOptionPane.jav @@ -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.ad 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 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 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.move 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. --- jedit5.7.0/jEdit/org/gjt/sp/jedit/options/StatusBarOptionPane.java 2024-08-03 1 +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/options/StatusBarOptionPane.java 202 @@ -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 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.move 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-patch --- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/RegisterViewer.java 2024-08-03 19:53:18.0 +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/RegisterViewer.java 2025-04-16 21 @@ -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 --- 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.098088 @@ -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-factor + 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/jE --- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/LogViewer.java 2024-08-03 19:53:16.000000 +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/LogViewer.java 2025-05-14 11:05:3 @@ -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.BL + 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.ORA errorColor = jEdit.getColorProperty("log-viewer.message.error.color", Color.RED); diff -ru /home/makarius/.isabelle/contrib/jedit-20250424/jedit5.7.0-patched/jEdit/ --- /home/makarius/.isabelle/contrib/jedit-20250424/jedit5.7.0-patched/jEdit/org/ +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/io/VFS.java 2025-05-14 10:51:16.53075 @@ -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/j --- jedit5.7.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2024-08-03 19:53:21.00000 +++ jedit5.7.0-patched/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2025-05-14 15:20: @@ -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", GUIUtilit + 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/ --- jedit5.7.0/jEdit/org/gjt/sp/jedit/EditPane.java 2024-08-03 19:53:15.000000000 +0 +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/EditPane.java 2025-11-28 19:22:09.823 @@ -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 buffe + public EditPane(@Nonnull View view, @Nullable BufferSet bufferSetSource, @Nonnull Buffe { 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.antiAlia - textArea.setMouseHandler(new MouseHandler(textArea)); + EditPaneMouseHandlerFactory mouseHandlerFactory = + ServiceManager.getService(EditPaneMouseHandlerFactory.class, "mouse-handler-fact + TextAreaMouseHandler mouseHandler = + mouseHandlerFactory == null ? new MouseHandler(textArea) : mouseHandlerFactory.create( + 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 --- jedit5.7.0/jEdit/org/gjt/sp/jedit/EditPaneMouseHandlerFactory.java 1970-01-01 0 +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/EditPaneMouseHandlerFactory.java 202 @@ -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 jedi --- jedit5.7.0/jEdit/org/gjt/sp/jedit/textarea/TextAreaMouseHandler.java 2024-08-0 +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextAreaMouseHandler.java 2 @@ -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/ --- /home/makarius/.isabelle/contrib/jedit-20250424/jedit5.7.0-patched/jEdit/org/ +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/NumericTextField.java 2025-05-14 @@ -95,7 +95,7 @@ Font font = getFont(); String family = font.getFamily(); int size = font.getSize(); - invalidStyle = SyntaxUtilities.parseStyle(jEdit.getProperty("view.style.invalid") + invalidStyle = SyntaxUtilities.parseStyle(jEdit.getThemeProperty("view.style.inva defaultForeground = getForeground(); defaultBackground = getBackground(); } diff -ru /home/makarius/.isabelle/contrib/jedit-20250424/jedit5.7.0-patched/jEdit/ --- /home/makarius/.isabelle/contrib/jedit-20250424/jedit5.7.0-patched/jEdit/org/ +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/statusbar/ErrorsWidgetFactory.j @@ -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 jedi --- jedit5.7.0/jEdit/org/gjt/sp/jedit/options/SyntaxHiliteOptionPane.java 2024-08- +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/options/SyntaxHiliteOptionPane.java @@ -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/ --- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java 2024-08-03 19:53:18.0000 +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/StyleEditor.java 2025-05-14 15:48 @@ -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.getStyleS jEdit.propertiesChanged(); } } //}}} diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/search/SearchBar.java jedit5.7.0-patched --- jedit5.7.0/jEdit/org/gjt/sp/jedit/search/SearchBar.java 2024-08-03 19:53:18.000 +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/search/SearchBar.java 2025-05-14 15:4 @@ -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.inval + SyntaxStyle style = SyntaxUtilities.parseStyle(jEdit.getThemeProperty("view.style. 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-patch --- jedit5.7.0/jEdit/org/gjt/sp/jedit/help/HistoryButton.java 2024-08-03 19:53:20.0 +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/help/HistoryButton.java 2025-05-20 15 @@ -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 + drop_button = new RolloverButton(GUIUtilities.loadIcon(jEdit.getThemeProperty("dro 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-patche --- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/OptionsDialog.java 2024-08-03 19:53:18.00 +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/OptionsDialog.java 2025-05-20 16: @@ -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 --- jedit5.7.0/jEdit/org/jedit/options/OptionGroupPane.java 2024-08-03 19:53:23.000 +++ jedit5.7.0-patched/jEdit/org/jedit/options/OptionGroupPane.java 2025-05-20 16:3 @@ -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. --- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 2024-08-03 1 +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java 202 @@ -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 DockableWindowContaine -{ +public class FloatingWindowContainer extends JDialog implements DockableWindowContain 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. --- jedit5.7.0/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java 2024-08-03 19:5 +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java 2025-0 @@ -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 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-pat --- jedit5.7.0/jEdit/org/gjt/sp/jedit/browser/BrowserView.java 2024-08-03 19:53:15. +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/browser/BrowserView.java 2025-08-25 2 @@ -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, parentDirectories.getSelectionModel().setSelectionMode(ListSelectionModel.SINGLE 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 en + 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-patc --- jedit5.7.0/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java 2024-08-03 19:53:15.0 +++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java 2025-08-25 21 @@ -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, "Fi filterCheckbox.setMargin(new Insets(0,0,0,0)); --> -------------------- --> maximum size reached --> -------------------- [ Verzeichnis aufwärts0.131unsichere Verbindung ] |
2026-03-28