# HG changeset patch
# User wenzelm
# Date 1376071310 -7200
# Node ID 4b053d8d0e7e2ea8d6b27210e57e30adca907ab3
# Parent  14ddcc0ad7df012aadbd178746e5af347303072b
removed "Locate" button, to avoid confusion about the slightly odd meaning of current_command with explicit theory context;

diff -r 14ddcc0ad7df -r 4b053d8d0e7e src/Tools/jEdit/src/find_dockable.scala
--- 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)
 }