src/Tools/jEdit/src/pretty_text_area.scala

   def detach
   {
     Swing_Thread.require {}
     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 */
 
   val search_label: Component = new Label("Search:") {