--- 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)
}
}))