# HG changeset patch
# User wenzelm
# Date 1399300149 -7200
# Node ID c4512e94e15c467b027ded15259a4dbf461eeb81
# Parent  168766e28f5e2aba64b861115eb83a2fb0385e40
tuned GUI;

diff -r 168766e28f5e -r c4512e94e15c 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 =