src/Tools/jEdit/src/pretty_text_area.scala

--- a/src/Tools/jEdit/src/pretty_text_area.scala	Thu May 08 21:03:05 2014 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Thu May 08 21:14:25 2014 +0200
@@ -177,6 +177,9 @@
     Info_Dockable(view, current_base_snapshot, current_base_results, current_body)
   }
 
+  def detach_operation: Option[() => Unit] =
+    if (current_body.isEmpty) None else Some(() => detach)
+
 
   /* common GUI components */