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