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