--- 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 =