# HG changeset patch # User wenzelm # Date 1273505359 -7200 # Node ID 55025bd6605f2670b034e060de98b509d00d771f # Parent cf36fd1e4cdac5eb4fd89b72a60a2bf0e2928477 more convenient get_font; diff -r cf36fd1e4cda -r 55025bd6605f src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Mon May 10 17:07:47 2010 +0200 +++ b/src/Pure/System/isabelle_system.scala Mon May 10 17:29:19 2010 +0200 @@ -318,8 +318,8 @@ val font_family = "IsabelleText" - def get_font(bold: Boolean): Font = - new Font(font_family, if (bold) Font.BOLD else Font.PLAIN, 1) + def get_font(bold: Boolean = false, size: Int = 1): Font = + new Font(font_family, if (bold) Font.BOLD else Font.PLAIN, size) def install_fonts() {