# HG changeset patch
# User wenzelm
# Date 1744842358 -7200
# Node ID f67ad2dbf6d5834310600d8ec5ee60762f5b5d19
# Parent  c98e22c67e21efda773847c4009cc832eca34d6f
tuned icons -- requires to update jedit component;

diff -r c98e22c67e21 -r f67ad2dbf6d5 src/Pure/Admin/component_jedit.scala
--- a/src/Pure/Admin/component_jedit.scala	Thu Apr 17 00:07:15 2025 +0200
+++ b/src/Pure/Admin/component_jedit.scala	Thu Apr 17 00:25:58 2025 +0200
@@ -376,10 +376,8 @@
 metal.secondary.fontsize=12
 navigate-backwards.label=Navigate backwards
 navigate-backwards.shortcut=AS+LEFT
-navigate-backwards.icon=ArrowL.png
 navigate-forwards.label=Navigate forwards
 navigate-forwards.shortcut=AS+RIGHT
-navigate-forwards.icon=ArrowR.png
 navigate-toolbar=navigate-backwards navigate-forwards
 navigator.showOnToolbar=true
 new-file-in-mode.shortcut=
diff -r c98e22c67e21 -r f67ad2dbf6d5 src/Tools/jEdit/patches/icons
--- a/src/Tools/jEdit/patches/icons	Thu Apr 17 00:07:15 2025 +0200
+++ b/src/Tools/jEdit/patches/icons	Thu Apr 17 00:25:58 2025 +0200
@@ -148,8 +148,8 @@
  		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-04-17 00:01:14.063978204 +0200
-@@ -8,11 +8,11 @@
++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/jedit_gui.props	2025-04-17 00:11:31.583536114 +0200
+@@ -8,13 +8,15 @@
  ###
  
  #{{{ Common icons
@@ -165,8 +165,12 @@
 +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,7 +28,7 @@
+ #}}}
+ 
+@@ -28,7 +30,7 @@
  defer=false
  startup=true
  
@@ -175,7 +179,7 @@
  dropdown-arrow.icon=ToolbarMenu.gif
  #}}}
  
-@@ -39,68 +39,69 @@
+@@ -39,68 +41,69 @@
  	buffer-options combined-options - \
  	plugin-manager - help
  
@@ -296,7 +300,7 @@
  	22x22/actions/application-run.png \
  	22x22/actions/edit-find-multiple.png \
  	22x22/actions/edit-find-single.png \
-@@ -109,18 +110,18 @@
+@@ -109,18 +112,18 @@
  	22x22/actions/window-unsplit.png \
  	22x22/actions/zoom-in.png \
  	22x22/actions/zoom-out.png \
@@ -326,7 +330,7 @@
  	Blank24.gif
  #}}}
  
-@@ -163,31 +164,31 @@
+@@ -163,31 +166,31 @@
  	 print \
  	 - \
  	 exit
@@ -377,7 +381,7 @@
  #}}}
  
  #{{{ Edit menu
-@@ -211,12 +212,12 @@
+@@ -211,12 +214,12 @@
  	 %text \
  	 %indent \
  	 %source
@@ -396,7 +400,7 @@
  
  #{{{ More Clipboard menu
  clipboard=cut-append \
-@@ -308,16 +309,18 @@
+@@ -308,16 +311,18 @@
  	   regexp \
  	   - \
  	   hypersearch-results
@@ -425,7 +429,7 @@
  #}}}
  
  #{{{ Markers menu
-@@ -336,12 +339,12 @@
+@@ -336,12 +341,12 @@
  	  view-markers \
  	  -
  markers.code=new MarkersProvider();
@@ -444,7 +448,7 @@
  #}}}
  
  #{{{ Folding menu
-@@ -388,9 +391,12 @@
+@@ -388,9 +393,12 @@
  	 - \
  	 set-view-title \
  	 toggle-full-screen
@@ -460,7 +464,7 @@
  
  #{{{ Scrolling menu
  scrolling=scroll-to-current-line \
-@@ -454,9 +460,9 @@
+@@ -454,9 +462,9 @@
  	  - \
  	  %quick-options
  
@@ -473,7 +477,7 @@
  
  #{{{ Recent Directories menu
  recent-directories.code=new RecentDirectoriesProvider();
-@@ -518,9 +524,9 @@
+@@ -518,9 +526,9 @@
  	   rescan-macros \
  	   -
  macros.code=new MacrosProvider();
@@ -486,7 +490,7 @@
  #}}}
  
  #{{{ Plugins menu
-@@ -771,7 +777,7 @@
+@@ -771,7 +779,7 @@
  
  #{{{ HyperSearch results dialog
  hypersearch-results.clear.icon=22x22/actions/edit-clear.png
@@ -495,7 +499,7 @@
  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 +790,8 @@
+@@ -784,8 +792,8 @@
  #}}}
  
  #{{{ Help Viewer
@@ -506,7 +510,7 @@
  #}}}
  
  #}}}
-@@ -809,9 +815,9 @@
+@@ -809,9 +817,9 @@
  
  #{{{ Abbreviations pane
  options.abbrevs.code=new AbbrevsOptionPane();
@@ -519,7 +523,7 @@
  #}}}
  
  #{{{ Appearance pane
-@@ -840,11 +846,11 @@
+@@ -840,11 +848,11 @@
  
  #{{{ Context Menu pane
  options.context.code=new ContextOptionPane();
@@ -536,7 +540,7 @@
  options.context.includeOptionsLink=true
  #}}}
  
-@@ -906,12 +912,12 @@
+@@ -906,12 +914,12 @@
  
  #{{{ Tool Bar pane
  options.toolbar.code=new ToolBarOptionPane();
@@ -555,7 +559,7 @@
  #}}}
  
  #{{{ View pane
-@@ -949,7 +955,8 @@
+@@ -949,7 +957,8 @@
  vfs.browser.default-filter=*[^~#]
  vfs.browser.filter-enabled=true
  vfs.browser.file.icon=16x16/mimetypes/text-x-generic.png
@@ -565,7 +569,7 @@
  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 +1014,13 @@
+@@ -1007,13 +1016,13 @@
  plugin-manager.mirror-url=http://plugins.jedit.org/export/mirror_list.php
  
  #{{{ Plugin management