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