equal
deleted
inserted
replaced
260 new Font(family, if (bold) Font.BOLD else Font.PLAIN, size) |
260 new Font(family, if (bold) Font.BOLD else Font.PLAIN, size) |
261 |
261 |
262 def install_fonts() |
262 def install_fonts() |
263 { |
263 { |
264 val ge = GraphicsEnvironment.getLocalGraphicsEnvironment() |
264 val ge = GraphicsEnvironment.getLocalGraphicsEnvironment() |
265 for (font <- Path.split(Isabelle_System.getenv_strict("ISABELLE_FONTS"))) |
265 for (font <- Isabelle_System.fonts()) |
266 ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, font.file)) |
266 ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, font.file)) |
267 } |
267 } |
268 } |
268 } |
269 |
269 |