tuned whitespace;
authorwenzelm
Sat, 13 Aug 2022 11:18:46 +0200
changeset 75833 8ffbd9343e91
parent 75832 1c0407b900db
child 75834 afa35ed14c71
tuned whitespace;
src/Tools/jEdit/src/output_dockable.scala
src/Tools/jEdit/src/simplifier_trace_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Sat Aug 13 11:18:22 2022 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Sat Aug 13 11:18:46 2022 +0200
@@ -83,7 +83,8 @@
   private val auto_update_button = new CheckBox("Auto update") {
     tooltip = "Indicate automatic update following cursor movement"
     reactions += {
-      case ButtonClicked(_) => do_update = this.selected; handle_update(do_update, None) }
+      case ButtonClicked(_) => do_update = this.selected; handle_update(do_update, None)
+    }
     selected = do_update
   }
 
--- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Sat Aug 13 11:18:22 2022 +0200
+++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Sat Aug 13 11:18:46 2022 +0200
@@ -149,28 +149,19 @@
         new CheckBox("Auto update") {
           selected = do_update
           reactions += {
-            case ButtonClicked(_) =>
-              do_update = this.selected
-              handle_update(do_update)
+            case ButtonClicked(_) => do_update = this.selected; handle_update(do_update)
           }
         },
         new Button("Update") {
-          reactions += {
-            case ButtonClicked(_) =>
-              handle_update(true)
-          }
+          reactions += { case ButtonClicked(_) => handle_update(true) }
         },
         new Separator(Orientation.Vertical),
         new Button("Show trace") {
-          reactions += {
-            case ButtonClicked(_) =>
-              show_trace()
-          }
+          reactions += { case ButtonClicked(_) => show_trace() }
         },
         new Button("Clear memory") {
           reactions += {
-            case ButtonClicked(_) =>
-              Simplifier_Trace.clear_memory(PIDE.session)
+            case ButtonClicked(_) => Simplifier_Trace.clear_memory(PIDE.session)
           }
         }))