added Output "Detach" button;

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