# HG changeset patch # User wenzelm # Date 1399555828 -7200 # Node ID dc3ba749d3b8ed0edffe71b0eb8c06429e5124c4 # Parent d1d986a9752464c6f292a44f538757a456eda537 tuned GUI; diff -r d1d986a97524 -r dc3ba749d3b8 src/Tools/jEdit/src/query_dockable.scala --- a/src/Tools/jEdit/src/query_dockable.scala Thu May 08 15:12:39 2014 +0200 +++ b/src/Tools/jEdit/src/query_dockable.scala Thu May 08 15:30:28 2014 +0200 @@ -113,6 +113,7 @@ private val allow_dups = new CheckBox("Duplicates") { tooltip = "Show all versions of matching theorems" selected = false + reactions += { case ButtonClicked(_) => apply_query() } } private val apply_button = new Button("Apply") {