# HG changeset patch
# User wenzelm
# Date 1350477540 -7200
# Node ID a6563caedf7a28e752ed740ce938795f418706fa
# Parent  89eff795f75782b08d378b430fe99d7f521c6616
added Output "Detach" button;

diff -r 89eff795f757 -r a6563caedf7a src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Wed Oct 17 14:20:54 2012 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Wed Oct 17 14:39:00 2012 +0200
@@ -169,6 +169,15 @@
   }
   update.tooltip = "Update display according to the command at cursor position"
 
-  private val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, tracing, auto_update, update)
+  private val detach = new Button("Detach") {
+    reactions += {
+      case ButtonClicked(_) =>
+        Info_Dockable(view, current_snapshot, Pretty.separate(current_output))
+    }
+  }
+  detach.tooltip = "Detach window with static copy of current output"
+
+  private val controls =
+    new FlowPanel(FlowPanel.Alignment.Right)(zoom, tracing, auto_update, update, detach)
   add(controls.peer, BorderLayout.NORTH)
 }