# HG changeset patch
# User wenzelm
# Date 1375820872 -7200
# Node ID 91f7fcaa214777916e51b430fa3ca9880d75c73b
# Parent  1df5280f8713731e031131c86f8ccd806fee330e
more generic button;

diff -r 1df5280f8713 -r 91f7fcaa2147 src/Tools/jEdit/src/find_dockable.scala
--- 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)
 }