# HG changeset patch
# User wenzelm
# Date 1743674653 -7200
# Node ID 0fc508521b2aa06258fe3f5fb0b0f39037ea657b
# Parent  955c5d6c1acf7574da8a385720be0deb94789b0b
add navigation buttons to search bar, depending on property "navigate-toolbar" -- requires to update jedit component;

diff -r 955c5d6c1acf -r 0fc508521b2a src/Pure/Admin/component_jedit.scala
--- a/src/Pure/Admin/component_jedit.scala	Wed Apr 02 23:22:59 2025 +0200
+++ b/src/Pure/Admin/component_jedit.scala	Thu Apr 03 12:04:13 2025 +0200
@@ -342,8 +342,11 @@
 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=
 next-bracket.shortcut2=C+e C+9
diff -r 955c5d6c1acf -r 0fc508521b2a src/Tools/jEdit/patches/search_bar
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/search_bar	Thu Apr 03 12:04:13 2025 +0200
@@ -0,0 +1,14 @@
+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-04-03 11:33:23.921426197 +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);
+