src/Pure/GUI/gui.scala
changeset 69355 cdc2de88d657
parent 69343 395c4fb15ea2
child 69357 acd0d72c560b
equal deleted inserted replaced
69354:600727ff6889 69355:cdc2de88d657
   240     new Font(family, if (bold) Font.BOLD else Font.PLAIN, size)
   240     new Font(family, if (bold) Font.BOLD else Font.PLAIN, size)
   241 
   241 
   242   def install_fonts()
   242   def install_fonts()
   243   {
   243   {
   244     val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
   244     val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
   245     for (font <- Isabelle_System.fonts())
   245     for (path <- Isabelle_Fonts.files())
   246       ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, font.file))
   246       ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, path.file))
   247   }
   247   }
   248 }
   248 }
   249 
   249