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() { JEdit_Lib.request_focus_view(view) } |
26 |
26 |
27 def set_content(c: Component) { add(c, BorderLayout.CENTER) } |
27 def set_content(c: Component) { 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) { add(c.peer, BorderLayout.CENTER) } |
29 |
29 |
30 def detach_operation: Option[() => Unit] = None |
30 def detach_operation: Option[() => Unit] = None |