src/Tools/jEdit/src/query_dockable.scala

     private def apply_query()
     {
       query_operation.apply_query(List(limit.text, allow_dups.selected.toString, query.getText))
     }
 
-    private val query_label = new Label("Search criteria:") {
+    private val query_label = new Label("Query:") {
       tooltip =
         GUI.tooltip_lines(
           "Search criteria for find operation, e.g.\n\"_ = _\" \"op +\" name: Group -name: monoid")
     }
 

     private val apply_button = new Button("Apply") {
       tooltip = "Find theorems meeting specified criteria"
       reactions += { case ButtonClicked(_) => apply_query() }
     }
 
-    private val detach = pretty_text_area.make_detach_button
-
     private val control_panel =
       new Wrap_Panel(Wrap_Panel.Alignment.Right)(
         query_label, Component.wrap(query), limit, allow_dups,
-        process_indicator.component, apply_button, detach)
+        process_indicator.component, apply_button,
+        pretty_text_area.search_label, pretty_text_area.search_pattern,
+        pretty_text_area.detach_button)
 
     def select { control_panel.contents += zoom }
 
     val page =
       new TabbedPane.Page("Find Theorems", new BorderPanel {

     private def apply_query()
     {
       query_operation.apply_query(List(query.getText))
     }
 
-    private val query_label = new Label("Search criteria:") {
+    private val query_label = new Label("Query:") {
       tooltip = GUI.tooltip_lines("Name / type patterns for constants")
     }
 
     val query = make_query("isabelle-find-consts", query_label.tooltip, apply_query _)
 

     private val apply_button = new Button("Apply") {
       tooltip = "Find constants by name / type patterns"
       reactions += { case ButtonClicked(_) => apply_query() }
     }
 
-    private val detach = pretty_text_area.make_detach_button
-
     private val control_panel =
       new Wrap_Panel(Wrap_Panel.Alignment.Right)(
-        query_label, Component.wrap(query), process_indicator.component, apply_button, detach)
+        query_label, Component.wrap(query), process_indicator.component, apply_button,
+        pretty_text_area.search_label, pretty_text_area.search_pattern,
+        pretty_text_area.detach_button)
 
     def select { control_panel.contents += zoom }
 
     val page =
       new TabbedPane.Page("Find Constants", new BorderPanel {

     private val apply_button = new Button("Apply") {
       tooltip = "Apply to current context"
       reactions += { case ButtonClicked(_) => apply_query() }
     }
 
-    private val detach = pretty_text_area.make_detach_button
-
     private val control_panel = new Wrap_Panel(Wrap_Panel.Alignment.Right)()
 
     def select
     {
       set_selector()
       control_panel.contents.clear
-      control_panel.contents ++= List(query_label, selector, apply_button, detach, zoom)
+      control_panel.contents ++=
+        List(query_label, selector, apply_button,
+          pretty_text_area.search_label, pretty_text_area.search_pattern,
+          pretty_text_area.detach_button, zoom)
     }
 
     val page =
       new TabbedPane.Page("Print Context", new BorderPanel {
         add(control_panel, BorderPanel.Position.North)