diff -r b3ca4a6ed74b -r 87ebf5a50283 src/Tools/jEdit/src/pide_docking_framework.scala --- a/src/Tools/jEdit/src/pide_docking_framework.scala Fri Apr 01 11:51:42 2022 +0200 +++ b/src/Tools/jEdit/src/pide_docking_framework.scala Fri Apr 01 17:06:10 2022 +0200 @@ -19,19 +19,17 @@ FloatingWindowContainer, PanelWindowContainer} -class PIDE_Docking_Framework extends DockableWindowManagerProvider -{ +class PIDE_Docking_Framework extends DockableWindowManagerProvider { override def create( view: View, instance: DockableWindowFactory, config: View.ViewConfig): DockableWindowManager = - new DockableWindowManagerImpl(view, instance, config) - { + new DockableWindowManagerImpl(view, instance, config) { override def createPopupMenu( container: DockableWindowContainer, dockable_name: String, - clone: Boolean): JPopupMenu = - { + clone: Boolean + ): JPopupMenu = { val menu = super.createPopupMenu(container, dockable_name, clone) val detach_operation: Option[() => Unit] =