# HG changeset patch
# User wenzelm
# Date 1399390138 -7200
# Node ID 15e18540df10494effe627992ac9d0747e344465
# Parent  f8c1d258369976acaa373379b57762b61128a64f
more uniform detach button;

diff -r f8c1d2583699 -r 15e18540df10 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Tue May 06 17:16:36 2014 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Tue May 06 17:28:58 2014 +0200
@@ -140,10 +140,7 @@
     reactions += { case ButtonClicked(_) => handle_update(true, None) }
   }
 
-  private val detach = new Button("Detach") {
-    tooltip = "Detach window with static copy of current output"
-    reactions += { case ButtonClicked(_) => pretty_text_area.detach }
-  }
+  private val detach = pretty_text_area.make_detach_button
 
   private val controls =
     new Wrap_Panel(Wrap_Panel.Alignment.Right)(auto_update, update, detach, zoom)
diff -r f8c1d2583699 -r 15e18540df10 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Tue May 06 17:16:36 2014 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Tue May 06 17:28:58 2014 +0200
@@ -14,6 +14,9 @@
 import java.awt.event.KeyEvent
 import java.util.concurrent.{Future => JFuture}
 
+import scala.swing.event.ButtonClicked
+import scala.swing.Button
+
 import org.gjt.sp.jedit.{jEdit, View, Registers}
 import org.gjt.sp.jedit.textarea.{AntiAlias, JEditEmbeddedTextArea}
 import org.gjt.sp.jedit.syntax.SyntaxStyle
@@ -167,6 +170,14 @@
   }
 
 
+  /* common GUI components */
+
+  def make_detach_button: Button = new Button("Detach") {
+    tooltip = "Detach window with static copy of current output"
+    reactions += { case ButtonClicked(_) => text_area.detach }
+  }
+
+
   /* key handling */
 
   addKeyListener(JEdit_Lib.key_listener(
diff -r f8c1d2583699 -r 15e18540df10 src/Tools/jEdit/src/query_dockable.scala
--- a/src/Tools/jEdit/src/query_dockable.scala	Tue May 06 17:16:36 2014 +0200
+++ b/src/Tools/jEdit/src/query_dockable.scala	Tue May 06 17:28:58 2014 +0200
@@ -36,14 +36,12 @@
   /* common GUI components */
 
   private var zoom_factor = 100
-
   private val zoom =
     new GUI.Zoom_Box(factor => if (zoom_factor != factor) { zoom_factor = factor; handle_resize() })
     {
       tooltip = "Zoom factor for output font size"
     }
 
-
   private def make_query(property: String, tooltip: String, apply_query: () => Unit): JTextField =
     new Completion_Popup.History_Text_Field(property)
     {
@@ -122,10 +120,12 @@
       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)
+        process_indicator.component, apply_button, detach)
 
     def select { control_panel.contents += zoom }
 
@@ -170,9 +170,11 @@
       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)
+        query_label, Component.wrap(query), process_indicator.component, apply_button, detach)
 
     def select { control_panel.contents += zoom }
 
@@ -251,13 +253,15 @@
       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, zoom)
+      control_panel.contents ++= List(query_label, _selector, apply_button, detach, zoom)
     }
 
     val page =