# HG changeset patch
# User wenzelm
# Date 1399576465 -7200
# Node ID a442dc6d244d1fd9d443816da3183da8b56ad77a
# Parent  7b65f4da136dded1ce661b89b68c364f64d6912a
clarified detach_operation: ignore empty output;

diff -r 7b65f4da136d -r a442dc6d244d src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Thu May 08 21:03:05 2014 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Thu May 08 21:14:25 2014 +0200
@@ -38,7 +38,7 @@
   val pretty_text_area = new Pretty_Text_Area(view)
   set_content(pretty_text_area)
 
-  override val detach_operation = Some(() => pretty_text_area.detach)
+  override def detach_operation = pretty_text_area.detach_operation
 
 
   private def handle_resize()
diff -r 7b65f4da136d -r a442dc6d244d 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 */
 
diff -r 7b65f4da136d -r a442dc6d244d src/Tools/jEdit/src/query_dockable.scala
--- a/src/Tools/jEdit/src/query_dockable.scala	Thu May 08 21:03:05 2014 +0200
+++ b/src/Tools/jEdit/src/query_dockable.scala	Thu May 08 21:14:25 2014 +0200
@@ -298,7 +298,11 @@
   select_operation()
   set_content(operations_pane)
 
-  override val detach_operation = Some(() => get_operation().foreach(_.pretty_text_area.detach))
+  override def detach_operation =
+    get_operation() match {
+      case None => None
+      case Some(op) => op.pretty_text_area.detach_operation
+    }
 
 
   /* resize */
diff -r 7b65f4da136d -r a442dc6d244d src/Tools/jEdit/src/sledgehammer_dockable.scala
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Thu May 08 21:03:05 2014 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Thu May 08 21:14:25 2014 +0200
@@ -24,6 +24,8 @@
   val pretty_text_area = new Pretty_Text_Area(view)
   set_content(pretty_text_area)
 
+  override def detach_operation = pretty_text_area.detach_operation
+
 
   /* query operation */