# HG changeset patch
# User wenzelm
# Date 1747751085 -7200
# Node ID 8be3035c82d4816fd060258e2d90b32cbeb901a8
# Parent  9f85679fd8998c20bba02f7e8145f9f86bd92e62
more scalable icons -- requires to update jedit component;

diff -r 9f85679fd899 -r 8be3035c82d4 src/Tools/jEdit/patches/gui
--- a/src/Tools/jEdit/patches/gui	Tue May 20 15:32:24 2025 +0200
+++ b/src/Tools/jEdit/patches/gui	Tue May 20 16:24:45 2025 +0200
@@ -1,6 +1,6 @@
 diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/GUIUtilities.java
 --- jedit5.7.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java	2024-08-03 19:53:15.000000000 +0200
-+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/GUIUtilities.java	2025-05-14 11:07:16.919569611 +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.*;
@@ -150,6 +150,15 @@
  			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 @@
  	}
  	//}}}