# HG changeset patch
# User wenzelm
# Date 1660296369 -7200
# Node ID f1a89044a7123582c6fe8672850f48ba74d8e0f8
# Parent  b0394e7d43eaa7af2d7e8d35de90d2c97810966a
tuned signature;

diff -r b0394e7d43ea -r f1a89044a712 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Fri Aug 12 11:18:22 2022 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Fri Aug 12 11:26:09 2022 +0200
@@ -136,13 +136,13 @@
     refresh()
   }
 
-  def detach: Unit = {
+  def detach(): Unit = {
     GUI_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)
+    if (current_body.isEmpty) None else Some(() => detach())
 
 
   /* common GUI components */