# HG changeset patch
# User wenzelm
# Date 1660296944 -7200
# Node ID 1dd5d4f4b69e7be24378822076b23d8ecf7aaccb
# Parent  f1a89044a7123582c6fe8672850f48ba74d8e0f8
tuned signature;

diff -r f1a89044a712 -r 1dd5d4f4b69e src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Fri Aug 12 11:26:09 2022 +0200
+++ b/src/Pure/GUI/gui.scala	Fri Aug 12 11:35:44 2022 +0200
@@ -118,7 +118,7 @@
   abstract class Zoom_Box extends ComboBox[String](
     List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%")
   ) {
-    def changed: Unit
+    def changed(): Unit
     def factor: Int = parse(selection.item)
 
     private def parse(text: String): Int =
@@ -147,7 +147,7 @@
     selection.index = 3
 
     listenTo(selection)
-    reactions += { case SelectionChanged(_) => changed }
+    reactions += { case SelectionChanged(_) => changed() }
   }
 
 
diff -r f1a89044a712 -r 1dd5d4f4b69e src/Tools/Graphview/graph_panel.scala
--- a/src/Tools/Graphview/graph_panel.scala	Fri Aug 12 11:26:09 2022 +0200
+++ b/src/Tools/Graphview/graph_panel.scala	Fri Aug 12 11:35:44 2022 +0200
@@ -298,7 +298,7 @@
     tooltip = "Save current graph layout as PNG or PDF"
   }
 
-  private val zoom = new GUI.Zoom_Box { def changed = rescale(0.01 * factor) }
+  private val zoom = new GUI.Zoom_Box { def changed() = rescale(0.01 * factor) }
 
   private val fit_window = new Button {
     action = Action("Fit to window") { fit_to_window() }
diff -r f1a89044a712 -r 1dd5d4f4b69e src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Fri Aug 12 11:26:09 2022 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Fri Aug 12 11:35:44 2022 +0200
@@ -268,7 +268,7 @@
     selected = false
   }
 
-  private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
+  private val zoom = new Font_Info.Zoom_Box { def changed() = handle_resize() }
 
   private val controls =
     Wrap_Panel(
diff -r f1a89044a712 -r 1dd5d4f4b69e src/Tools/jEdit/src/info_dockable.scala
--- a/src/Tools/jEdit/src/info_dockable.scala	Fri Aug 12 11:26:09 2022 +0200
+++ b/src/Tools/jEdit/src/info_dockable.scala	Fri Aug 12 11:35:44 2022 +0200
@@ -72,7 +72,7 @@
 
   pretty_text_area.update(snapshot, results, info)
 
-  private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
+  private val zoom = new Font_Info.Zoom_Box { def changed() = handle_resize() }
 
   private def handle_resize(): Unit = {
     GUI_Thread.require {}
diff -r f1a89044a712 -r 1dd5d4f4b69e src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Fri Aug 12 11:26:09 2022 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Fri Aug 12 11:35:44 2022 +0200
@@ -96,7 +96,7 @@
     reactions += { case ButtonClicked(_) => handle_update(true, None) }
   }
 
-  private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
+  private val zoom = new Font_Info.Zoom_Box { def changed() = handle_resize() }
 
   private val controls =
     Wrap_Panel(
diff -r f1a89044a712 -r 1dd5d4f4b69e src/Tools/jEdit/src/query_dockable.scala
--- a/src/Tools/jEdit/src/query_dockable.scala	Fri Aug 12 11:26:09 2022 +0200
+++ b/src/Tools/jEdit/src/query_dockable.scala	Fri Aug 12 11:35:44 2022 +0200
@@ -24,7 +24,7 @@
     val pretty_text_area = new Pretty_Text_Area(view)
     def query_operation: Query_Operation[View]
     def query: JComponent
-    def select: Unit
+    def select(): Unit
     def page: TabbedPane.Page
   }
 }
@@ -32,7 +32,7 @@
 class Query_Dockable(view: View, position: String) extends Dockable(view, position) {
   /* common GUI components */
 
-  private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
+  private val zoom = new Font_Info.Zoom_Box { def changed() = handle_resize() }
 
   private def make_query(
     property: String,
@@ -124,7 +124,7 @@
           process_indicator.component, apply_button,
           pretty_text_area.search_label, pretty_text_area.search_field))
 
-    def select: Unit = { control_panel.contents += zoom }
+    def select(): Unit = { control_panel.contents += zoom }
 
     val page =
       new TabbedPane.Page("Find Theorems", new BorderPanel {
@@ -173,7 +173,7 @@
           query_label, Component.wrap(query), process_indicator.component, apply_button,
           pretty_text_area.search_label, pretty_text_area.search_field))
 
-    def select: Unit = { control_panel.contents += zoom }
+    def select(): Unit = { control_panel.contents += zoom }
 
     val page =
       new TabbedPane.Page("Find Constants", new BorderPanel {
@@ -250,7 +250,7 @@
 
     private val control_panel = Wrap_Panel()
 
-    def select: Unit = {
+    def select(): Unit = {
       control_panel.contents.clear()
       control_panel.contents += query_label
       update_items().foreach(item => control_panel.contents += item.checkbox)
@@ -282,7 +282,7 @@
     catch { case _: IndexOutOfBoundsException => None }
 
   private def select_operation(): Unit = {
-    for (op <- get_operation()) { op.select; op.query.requestFocus() }
+    for (op <- get_operation()) { op.select(); op.query.requestFocus() }
     operations_pane.revalidate()
   }
 
diff -r f1a89044a712 -r 1dd5d4f4b69e src/Tools/jEdit/src/simplifier_trace_window.scala
--- a/src/Tools/jEdit/src/simplifier_trace_window.scala	Fri Aug 12 11:26:09 2022 +0200
+++ b/src/Tools/jEdit/src/simplifier_trace_window.scala	Fri Aug 12 11:35:44 2022 +0200
@@ -133,7 +133,7 @@
   GUI_Thread.require {}
 
   private val pretty_text_area = new Pretty_Text_Area(view)
-  private val zoom = new Font_Info.Zoom_Box { def changed = do_paint() }
+  private val zoom = new Font_Info.Zoom_Box { def changed() = do_paint() }
 
   size = new Dimension(500, 500)
   contents = new BorderPanel {
diff -r f1a89044a712 -r 1dd5d4f4b69e src/Tools/jEdit/src/sledgehammer_dockable.scala
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Fri Aug 12 11:26:09 2022 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Fri Aug 12 11:35:44 2022 +0200
@@ -129,7 +129,7 @@
     reactions += { case ButtonClicked(_) => sledgehammer.locate_query() }
   }
 
-  private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
+  private val zoom = new Font_Info.Zoom_Box { def changed() = handle_resize() }
 
   private val controls =
     Wrap_Panel(
diff -r f1a89044a712 -r 1dd5d4f4b69e src/Tools/jEdit/src/state_dockable.scala
--- a/src/Tools/jEdit/src/state_dockable.scala	Fri Aug 12 11:26:09 2022 +0200
+++ b/src/Tools/jEdit/src/state_dockable.scala	Fri Aug 12 11:35:44 2022 +0200
@@ -98,7 +98,7 @@
     reactions += { case ButtonClicked(_) => print_state.locate_query() }
   }
 
-  private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
+  private val zoom = new Font_Info.Zoom_Box { def changed() = handle_resize() }
 
   private val controls =
     Wrap_Panel(