diff -r b0a30a21f627 -r e9fa94f43a15 src/Pure/GUI/wrap_panel.scala --- a/src/Pure/GUI/wrap_panel.scala Tue Jun 27 20:16:40 2017 +0200 +++ b/src/Pure/GUI/wrap_panel.scala Tue Jun 27 21:36:58 2017 +0200 @@ -100,18 +100,19 @@ } } } + + def apply(contents: List[Component] = Nil, + alignment: Wrap_Panel.Alignment.Value = Wrap_Panel.Alignment.Center): Wrap_Panel = + new Wrap_Panel(contents, alignment) } - -class Wrap_Panel(alignment: Wrap_Panel.Alignment.Value)(contents0: Component*) +class Wrap_Panel(contents0: List[Component] = Nil, + alignment: Wrap_Panel.Alignment.Value = Wrap_Panel.Alignment.Center) extends Panel with SequentialContainer.Wrapper { override lazy val peer: JPanel = new JPanel(new Wrap_Panel.Layout(alignment.id)) with SuperMixin - def this(contents0: Component*) = this(Wrap_Panel.Alignment.Center)(contents0: _*) - def this() = this(Wrap_Panel.Alignment.Center)() - contents ++= contents0 private def layoutManager = peer.getLayout.asInstanceOf[Wrap_Panel.Layout]