# HG changeset patch
# User wenzelm
# Date 1399554759 -7200
# Node ID d1d986a9752464c6f292a44f538757a456eda537
# Parent a1557dc7f589d32195359ace27ea3a2833eeac5a
tuned GUI;
diff -r a1557dc7f589 -r d1d986a97524 src/Tools/jEdit/src/query_dockable.scala
--- a/src/Tools/jEdit/src/query_dockable.scala Thu May 08 14:53:04 2014 +0200
+++ b/src/Tools/jEdit/src/query_dockable.scala Thu May 08 15:12:39 2014 +0200
@@ -115,7 +115,7 @@
selected = false
}
- private val apply_button = new Button("Apply") {
+ private val apply_button = new Button("Apply") {
tooltip = "Find theorems meeting specified criteria"
reactions += { case ButtonClicked(_) => apply_query() }
}
@@ -164,7 +164,7 @@
/* GUI page */
- private val apply_button = new Button("Apply") {
+ private val apply_button = new Button("Apply") {
tooltip = "Find constants by name / type patterns"
reactions += { case ButtonClicked(_) => apply_query() }
}
@@ -248,7 +248,7 @@
/* GUI page */
- private val apply_button = new Button("Apply") {
+ private val apply_button = new Button("Apply") {
tooltip = "Apply to current context"
reactions += { case ButtonClicked(_) => apply_query() }
}