equal
deleted
inserted
replaced
20 extends JPanel(new BorderLayout) with DefaultFocusComponent |
20 extends JPanel(new BorderLayout) with DefaultFocusComponent |
21 { |
21 { |
22 if (position == DockableWindowManager.FLOATING) |
22 if (position == DockableWindowManager.FLOATING) |
23 setPreferredSize(new Dimension(500, 250)) |
23 setPreferredSize(new Dimension(500, 250)) |
24 |
24 |
25 def focusOnDefaultComponent() { JEdit_Lib.request_focus_view(view) } |
25 def focusOnDefaultComponent(): Unit = JEdit_Lib.request_focus_view(view) |
26 |
26 |
27 def set_content(c: Component) { add(c, BorderLayout.CENTER) } |
27 def set_content(c: Component): Unit = add(c, BorderLayout.CENTER) |
28 def set_content(c: scala.swing.Component) { add(c.peer, BorderLayout.CENTER) } |
28 def set_content(c: scala.swing.Component): Unit = add(c.peer, BorderLayout.CENTER) |
29 |
29 |
30 def detach_operation: Option[() => Unit] = None |
30 def detach_operation: Option[() => Unit] = None |
31 |
31 |
32 protected def init() { } |
32 protected def init(): Unit = {} |
33 protected def exit() { } |
33 protected def exit(): Unit = {} |
34 |
34 |
35 override def addNotify() |
35 override def addNotify(): Unit = |
36 { |
36 { |
37 super.addNotify() |
37 super.addNotify() |
38 init() |
38 init() |
39 } |
39 } |
40 |
40 |
41 override def removeNotify() |
41 override def removeNotify(): Unit = |
42 { |
42 { |
43 exit() |
43 exit() |
44 super.removeNotify() |
44 super.removeNotify() |
45 } |
45 } |
46 } |
46 } |