src/Pure/GUI/wrap_panel.scala
changeset 66206 2d2082db735a
parent 66205 e9fa94f43a15
child 68224 1f7308050349
equal deleted inserted replaced
66205:e9fa94f43a15 66206:2d2082db735a
   100       }
   100       }
   101     }
   101     }
   102   }
   102   }
   103 
   103 
   104   def apply(contents: List[Component] = Nil,
   104   def apply(contents: List[Component] = Nil,
   105       alignment: Wrap_Panel.Alignment.Value = Wrap_Panel.Alignment.Center): Wrap_Panel =
   105       alignment: Alignment.Value = Alignment.Right): Wrap_Panel =
   106     new Wrap_Panel(contents, alignment)
   106     new Wrap_Panel(contents, alignment)
   107 }
   107 }
   108 
   108 
   109 class Wrap_Panel(contents0: List[Component] = Nil,
   109 class Wrap_Panel(contents0: List[Component] = Nil,
   110     alignment: Wrap_Panel.Alignment.Value = Wrap_Panel.Alignment.Center)
   110     alignment: Wrap_Panel.Alignment.Value = Wrap_Panel.Alignment.Right)
   111   extends Panel with SequentialContainer.Wrapper
   111   extends Panel with SequentialContainer.Wrapper
   112 {
   112 {
   113   override lazy val peer: JPanel =
   113   override lazy val peer: JPanel =
   114     new JPanel(new Wrap_Panel.Layout(alignment.id)) with SuperMixin
   114     new JPanel(new Wrap_Panel.Layout(alignment.id)) with SuperMixin
   115 
   115