# HG changeset patch # User wenzelm # Date 1273523278 -7200 # Node ID 1fd4f28e6ce113514a346ca742bf4815ac4d0c1f # Parent f60e4dd6d76f982bd40a8bc155a87dd555ccefe4 more convenient get_font; diff -r f60e4dd6d76f -r 1fd4f28e6ce1 src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Mon May 10 20:53:06 2010 +0200 +++ b/src/Pure/System/isabelle_system.scala Mon May 10 22:27:58 2010 +0200 @@ -318,7 +318,7 @@ val font_family = "IsabelleText" - def get_font(bold: Boolean = false, size: Int = 1): Font = + def get_font(size: Int = 1, bold: Boolean = false): Font = new Font(font_family, if (bold) Font.BOLD else Font.PLAIN, size) def install_fonts() @@ -330,7 +330,7 @@ else "$ISABELLE_HOME/lib/fonts/IsabelleText.ttf" Font.createFont(Font.TRUETYPE_FONT, platform_file(name)) } - def check_font() = get_font(false).getFamily == font_family + def check_font() = get_font().getFamily == font_family if (!check_font()) { val font = create_font(false)