--- a/src/Tools/jEdit/src/find_dockable.scala Fri Aug 09 17:25:47 2013 +0200
+++ b/src/Tools/jEdit/src/find_dockable.scala Fri Aug 09 20:01:50 2013 +0200
@@ -151,11 +151,6 @@
reactions += { case ButtonClicked(_) => clicked }
}
- private val locate_query = new Button("Locate") {
- tooltip = "Locate context of current query within source text"
- reactions += { case ButtonClicked(_) => find_theorems.locate_query() }
- }
-
private val zoom = new GUI.Zoom_Box(factor => { zoom_factor = factor; handle_resize() }) {
tooltip = "Zoom factor for output font size"
}
@@ -163,6 +158,6 @@
private val controls =
new FlowPanel(FlowPanel.Alignment.Right)(
query_label, Component.wrap(query), context, limit, allow_dups,
- process_indicator.component, apply_query, locate_query, zoom)
+ process_indicator.component, apply_query, zoom)
add(controls.peer, BorderLayout.NORTH)
}