src/Tools/jEdit/src/symbols_dockable.scala
changeset 71601 97ccf48c2f0c
parent 67389 7e21d19e7ad7
child 71704 b9a5eb0f3b43
--- a/src/Tools/jEdit/src/symbols_dockable.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Tools/jEdit/src/symbols_dockable.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -174,7 +174,7 @@
     }
 
     for (page <- pages)
-      page.title = Word.implode(Word.explode('_', page.title).map(Word.perhaps_capitalize(_)))
+      page.title = Word.implode(Word.explode('_', page.title).map(Word.perhaps_capitalize))
   }
   set_content(group_tabs)
 
@@ -200,7 +200,7 @@
                 }
               case _ =>
             })
-          comp.revalidate
+          comp.revalidate()
           comp.repaint()
         }
       case _: Session.Commands_Changed => abbrevs_refresh_delay.invoke()