# HG changeset patch # User wenzelm # Date 1597316381 -7200 # Node ID 25db9c4209eee33e7f59aed92d8d04fd17fa5a12 # Parent 6a4e51ca53c3e01f1fae640278c1c124121f71c0 tuned GUI; diff -r 6a4e51ca53c3 -r 25db9c4209ee src/Tools/jEdit/src/monitor_dockable.scala --- a/src/Tools/jEdit/src/monitor_dockable.scala Thu Aug 13 12:53:51 2020 +0200 +++ b/src/Tools/jEdit/src/monitor_dockable.scala Thu Aug 13 12:59:41 2020 +0200 @@ -78,6 +78,13 @@ } } + private val limit_data = new TextField("200", 5) { + tooltip = "Limit for accumulated data" + verifier = (s: String) => + s match { case Value.Int(x) => x > 0 case _ => false } + reactions += { case ValueChanged(_) => input_delay.invoke() } + } + private val reset_data = new Button("Reset") { tooltip = "Reset accumulated data" reactions += { @@ -86,14 +93,7 @@ } } - private val limit_data = new TextField("200", 5) { - tooltip = "Limit for accumulated data" - verifier = (s: String) => - s match { case Value.Int(x) => x > 0 case _ => false } - reactions += { case ValueChanged(_) => input_delay.invoke() } - } - - private val controls = Wrap_Panel(List(select_data, reset_data, limit_data)) + private val controls = Wrap_Panel(List(select_data, limit_data, reset_data)) /* layout */