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