tuned GUI;
authorwenzelm
Mon, 05 May 2014 16:29:09 +0200
changeset 56866 c4512e94e15c
parent 56865 168766e28f5e
child 56867 224109105008
tuned GUI;
src/Tools/jEdit/src/find_dockable.scala
--- a/src/Tools/jEdit/src/find_dockable.scala	Mon May 05 15:37:25 2014 +0200
+++ b/src/Tools/jEdit/src/find_dockable.scala	Mon May 05 16:29:09 2014 +0200
@@ -208,6 +208,8 @@
       query_operation.apply_query(List(_selector.selection.item.name))
     }
 
+    private val query_label = new Label("Print:")
+
     def query: JComponent = _selector.peer.asInstanceOf[JComponent]
 
 
@@ -240,7 +242,7 @@
     {
       update_selector()
       control_panel.contents.clear
-      control_panel.contents ++= List(_selector, apply_button, zoom)
+      control_panel.contents ++= List(query_label, _selector, apply_button, zoom)
     }
 
     val page =