# HG changeset patch
# User wenzelm
# Date 1399389396 -7200
# Node ID f8c1d258369976acaa373379b57762b61128a64f
# Parent  ee2b61f37ad92848af8c3f046a9001ff3149ca59
tuned signature;

diff -r ee2b61f37ad9 -r f8c1d2583699 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Tue May 06 16:57:17 2014 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Tue May 06 17:16:36 2014 +0200
@@ -142,10 +142,7 @@
 
   private val detach = new Button("Detach") {
     tooltip = "Detach window with static copy of current output"
-    reactions += {
-      case ButtonClicked(_) =>
-        Info_Dockable(view, current_snapshot, current_results, Pretty.separate(current_output))
-    }
+    reactions += { case ButtonClicked(_) => pretty_text_area.detach }
   }
 
   private val controls =
diff -r ee2b61f37ad9 -r f8c1d2583699 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Tue May 06 16:57:17 2014 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Tue May 06 17:16:36 2014 +0200
@@ -160,6 +160,12 @@
     refresh()
   }
 
+  def detach
+  {
+    Swing_Thread.require {}
+    Info_Dockable(view, current_base_snapshot, current_base_results, current_body)
+  }
+
 
   /* key handling */