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 */