tuned GUI;
authorwenzelm
Thu, 13 Aug 2020 12:59:41 +0200
changeset 72145 25db9c4209ee
parent 72144 6a4e51ca53c3
child 72146 d8dd3aa6dae9
tuned GUI;
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 */