# HG changeset patch
# User wenzelm
# Date 1660297632 -7200
# Node ID 51867c8ad109ce33d2faec48af463d8907f3d1bc
# Parent  1dd5d4f4b69e7be24378822076b23d8ecf7aaccb
tuned, following hints by IntelliJ IDEA;

diff -r 1dd5d4f4b69e -r 51867c8ad109 src/Tools/Graphview/graph_panel.scala
--- a/src/Tools/Graphview/graph_panel.scala	Fri Aug 12 11:35:44 2022 +0200
+++ b/src/Tools/Graphview/graph_panel.scala	Fri Aug 12 11:47:12 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(): Unit = rescale(0.01 * factor) }
 
   private val fit_window = new Button {
     action = Action("Fit to window") { fit_to_window() }
diff -r 1dd5d4f4b69e -r 51867c8ad109 src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Fri Aug 12 11:35:44 2022 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Fri Aug 12 11:47:12 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(): Unit = handle_resize() }
 
   private val controls =
     Wrap_Panel(
diff -r 1dd5d4f4b69e -r 51867c8ad109 src/Tools/jEdit/src/info_dockable.scala
--- a/src/Tools/jEdit/src/info_dockable.scala	Fri Aug 12 11:35:44 2022 +0200
+++ b/src/Tools/jEdit/src/info_dockable.scala	Fri Aug 12 11:47:12 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(): Unit = handle_resize() }
 
   private def handle_resize(): Unit = {
     GUI_Thread.require {}
diff -r 1dd5d4f4b69e -r 51867c8ad109 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Fri Aug 12 11:35:44 2022 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Fri Aug 12 11:47:12 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(): Unit = handle_resize() }
 
   private val controls =
     Wrap_Panel(
diff -r 1dd5d4f4b69e -r 51867c8ad109 src/Tools/jEdit/src/query_dockable.scala
--- a/src/Tools/jEdit/src/query_dockable.scala	Fri Aug 12 11:35:44 2022 +0200
+++ b/src/Tools/jEdit/src/query_dockable.scala	Fri Aug 12 11:47:12 2022 +0200
@@ -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(): Unit = handle_resize() }
 
   private def make_query(
     property: String,
@@ -71,7 +71,7 @@
 
   /* find theorems */
 
-  private val find_theorems = new Query_Dockable.Operation(view) {
+  private val find_theorems: Query_Dockable.Operation = new Query_Dockable.Operation(view) {
     /* query */
 
     private val process_indicator = new Process_Indicator
@@ -101,8 +101,7 @@
 
     private val limit = new TextField(PIDE.options.int("find_theorems_limit").toString, 5) {
       tooltip = "Limit of displayed results"
-      verifier = (s: String) =>
-        s match { case Value.Int(x) => x >= 0 case _ => false }
+      verifier = { case Value.Int(x) => x >= 0 case _ => false }
       listenTo(keys)
       reactions += { case KeyPressed(_, Key.Enter, 0, _) => apply_query() }
     }
@@ -136,7 +135,7 @@
 
   /* find consts */
 
-  private val find_consts = new Query_Dockable.Operation(view) {
+  private val find_consts: Query_Dockable.Operation = new Query_Dockable.Operation(view) {
     /* query */
 
     private val process_indicator = new Process_Indicator
@@ -189,7 +188,7 @@
     /* items */
 
     private class Item(val name: String, description: String, sel: Boolean) {
-      val checkbox = new CheckBox(name) {
+      val checkbox: CheckBox = new CheckBox(name) {
         tooltip = "Print " + description
         selected = sel
         reactions += { case ButtonClicked(_) => apply_query() }
diff -r 1dd5d4f4b69e -r 51867c8ad109 src/Tools/jEdit/src/simplifier_trace_window.scala
--- a/src/Tools/jEdit/src/simplifier_trace_window.scala	Fri Aug 12 11:35:44 2022 +0200
+++ b/src/Tools/jEdit/src/simplifier_trace_window.scala	Fri Aug 12 11:47:12 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(): Unit = do_paint() }
 
   size = new Dimension(500, 500)
   contents = new BorderPanel {
diff -r 1dd5d4f4b69e -r 51867c8ad109 src/Tools/jEdit/src/sledgehammer_dockable.scala
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Fri Aug 12 11:35:44 2022 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Fri Aug 12 11:47:12 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(): Unit = handle_resize() }
 
   private val controls =
     Wrap_Panel(
diff -r 1dd5d4f4b69e -r 51867c8ad109 src/Tools/jEdit/src/state_dockable.scala
--- a/src/Tools/jEdit/src/state_dockable.scala	Fri Aug 12 11:35:44 2022 +0200
+++ b/src/Tools/jEdit/src/state_dockable.scala	Fri Aug 12 11:47:12 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(): Unit = handle_resize() }
 
   private val controls =
     Wrap_Panel(