--- 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)