tuned whitespace;

--- a/src/Tools/jEdit/src/monitor_dockable.scala	Sat Aug 13 11:53:45 2022 +0200
+++ b/src/Tools/jEdit/src/monitor_dockable.scala	Sat Aug 13 11:59:06 2022 +0200
@@ -67,11 +67,7 @@
   private val select_data = new ComboBox[String](ML_Statistics.all_fields.map(_._1)) {
     tooltip = "Select visualized data collection"
     listenTo(selection)
-    reactions += {
-      case SelectionChanged(_) =>
-        data_name = selection.item
-        update_chart()
-    }
+    reactions += { case SelectionChanged(_) => data_name = selection.item; update_chart() }
   }
 
   private val limit_data = new TextField("200", 5) {
@@ -85,11 +81,7 @@
 
   private val reset_data = new Button("Reset") {
     tooltip = "Reset accumulated data"
-    reactions += {
-      case ButtonClicked(_) =>
-        clear_statistics()
-        update_chart()
-    }
+    reactions += { case ButtonClicked(_) => clear_statistics(); update_chart() }
   }
 
   private val full_gc = new Button("GC") {