src/Pure/GUI/wrap_panel.scala
changeset 66205 e9fa94f43a15
parent 60033 9a1d40876e9f
child 66206 2d2082db735a
--- 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]