--- a/src/Tools/jEdit/src/find_dockable.scala Tue Aug 06 22:02:20 2013 +0200
+++ b/src/Tools/jEdit/src/find_dockable.scala Tue Aug 06 22:27:52 2013 +0200
@@ -99,12 +99,12 @@
private val query_wrapped = Component.wrap(query)
- private val find = new Button("Find") {
+ private val apply_query = new Button("Apply") {
tooltip = "Find theorems meeting specified criteria"
reactions += { case ButtonClicked(_) => find_theorems.apply_query(List(query.getText)) }
}
- private val locate = new Button("Locate") {
+ private val locate_query = new Button("Locate") {
tooltip = "Locate context of current query within source text"
reactions += { case ButtonClicked(_) => find_theorems.locate_query() }
}
@@ -115,6 +115,6 @@
private val controls =
new FlowPanel(FlowPanel.Alignment.Right)(
- query_wrapped, find_theorems.animation, find, locate, zoom)
+ query_wrapped, find_theorems.animation, apply_query, locate_query, zoom)
add(controls.peer, BorderLayout.NORTH)
}