equal
deleted
inserted
replaced
141 verifier = ((s: String) => |
141 verifier = ((s: String) => |
142 s match { case Value.Double(x) => x >= 0.0 case _ => false }) |
142 s match { case Value.Double(x) => x >= 0.0 case _ => false }) |
143 } |
143 } |
144 |
144 |
145 private val controls = |
145 private val controls = |
146 new Wrap_Panel(Wrap_Panel.Alignment.Right)(threshold_label, threshold_value) |
146 Wrap_Panel(List(threshold_label, threshold_value), Wrap_Panel.Alignment.Right) |
147 add(controls.peer, BorderLayout.NORTH) |
147 add(controls.peer, BorderLayout.NORTH) |
148 |
148 |
149 |
149 |
150 /* component state -- owned by GUI thread */ |
150 /* component state -- owned by GUI thread */ |
151 |
151 |