# HG changeset patch
# User wenzelm
# Date 1660384746 -7200
# Node ID 7f6803788de3aa01c4e6dfcd205a7b028aa3eff0
# Parent  93a704c52061b9b91aa7673d80e0aa4fc88ec82b
tuned whitespace;

diff -r 93a704c52061 -r 7f6803788de3 src/Tools/jEdit/src/monitor_dockable.scala
--- 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") {