clarified GUI: omit pointless search buttons, as real output is shown as markup;
authorwenzelm
Wed, 01 Feb 2023 13:50:53 +0100
changeset 77169 b2bc810e4bf7
parent 77168 547d140f0780
child 77170 2ddb82044ff0
clarified GUI: omit pointless search buttons, as real output is shown as markup;
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 {