# HG changeset patch
# User wenzelm
# Date 1743676634 -7200
# Node ID b684876ab760c86daf69f7a4826eec5b846f9e16
# Parent  0fc508521b2aa06258fe3f5fb0b0f39037ea657b
prefer search bar (with navigation buttons) over old-fashioned tool bar  -- requires to update jedit component;

diff -r 0fc508521b2a -r b684876ab760 src/Pure/Admin/component_jedit.scala
--- a/src/Pure/Admin/component_jedit.scala	Thu Apr 03 12:04:13 2025 +0200
+++ b/src/Pure/Admin/component_jedit.scala	Thu Apr 03 12:37:14 2025 +0200
@@ -412,7 +412,8 @@
 view.gutter.selectionAreaWidth=18
 view.height=850
 view.middleMousePaste=true
-view.showToolbar=true
+view.showSearchbar=true
+view.showToolbar=false
 view.status.memory.background=#666699
 view.status=( mode , fold , encoding ) locked wrap multiSelect rectSelect overwrite lineSep buffersets task-monitor java-status ml-status errors clock
 view.thickCaret=true