equal
deleted
inserted
replaced
131 case _ => |
131 case _ => |
132 } |
132 } |
133 handle_update() |
133 handle_update() |
134 } |
134 } |
135 tooltip = threshold_tooltip |
135 tooltip = threshold_tooltip |
136 verifier = ((s: String) => |
136 verifier = { case Value.Double(x) => x >= 0.0 case _ => false } |
137 s match { case Value.Double(x) => x >= 0.0 case _ => false }) |
|
138 } |
137 } |
139 |
138 |
140 private val controls = Wrap_Panel(List(threshold_label, threshold_value)) |
139 private val controls = Wrap_Panel(List(threshold_label, threshold_value)) |
141 |
140 |
142 add(controls.peer, BorderLayout.NORTH) |
141 add(controls.peer, BorderLayout.NORTH) |