src/Pure/GUI/gui.scala
changeset 73340 0ffcad1f6130
parent 73337 0af9e7e4476f
child 73367 77ef8bef0593
--- a/src/Pure/GUI/gui.scala	Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/GUI/gui.scala	Mon Mar 01 22:22:12 2021 +0100
@@ -36,7 +36,7 @@
   lazy val look_and_feels: List[Look_And_Feel] =
     Isabelle_System.make_services(classOf[Look_And_Feel])
 
-  def init_lafs()
+  def init_lafs(): Unit =
   {
     val old_lafs =
       Set(
@@ -54,7 +54,7 @@
 
   /* plain focus traversal, notably for text fields */
 
-  def plain_focus_traversal(component: Component)
+  def plain_focus_traversal(component: Component): Unit =
   {
     val dummy_button = new JButton
     def apply(id: Int): Unit =
@@ -78,7 +78,7 @@
   }
 
   private def simple_dialog(kind: Int, default_title: String,
-    parent: Component, title: String, message: Iterable[Any])
+    parent: Component, title: String, message: Iterable[Any]): Unit =
   {
     GUI_Thread.now {
       val java_message =
@@ -127,7 +127,8 @@
 
     private def print(i: Int): String = i.toString + "%"
 
-    def set_item(i: Int) {
+    def set_item(i: Int): Unit =
+    {
       peer.getEditor match {
         case null =>
         case editor => editor.setItem(print(i))
@@ -272,9 +273,9 @@
       case _ => None
     }
 
-  def traverse_components(component: Component, apply: Component => Unit)
+  def traverse_components(component: Component, apply: Component => Unit): Unit =
   {
-    def traverse(comp: Component)
+    def traverse(comp: Component): Unit =
     {
       apply(comp)
       comp match {
@@ -326,7 +327,7 @@
     "font-family: " + family + "; font-size: " + (scale * rel_size * 100).toInt + "%;"
   }
 
-  def use_isabelle_fonts()
+  def use_isabelle_fonts(): Unit =
   {
     val default_font = label_font()
     val ui = UIManager.getDefaults