# HG changeset patch
# User wenzelm
# Date 1675255853 -3600
# Node ID b2bc810e4bf70feb871e52bf0d558071666e403f
# Parent  547d140f07803326cb76d41ad37f2c14c878882e
clarified GUI: omit pointless search buttons, as real output is shown as markup;

diff -r 547d140f0780 -r b2bc810e4bf7 src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Wed Feb 01 10:54:29 2023 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Wed Feb 01 13:50:53 2023 +0100
@@ -371,8 +371,7 @@
       layout(theories_pane) = BorderPanel.Position.Center
     }, "Selection and status of document theories")
 
-  private val output_controls =
-    Wrap_Panel(List(pretty_text_area.search_label, pretty_text_area.search_field, zoom))
+  private val output_controls = Wrap_Panel(List(zoom))
 
   private val output_page =
     new TabbedPane.Page("Output", new BorderPanel {