src/Pure/GUI/gui.scala
changeset 65083 9a0e34edfad1
parent 63874 e2393cfde472
child 65370 1324268c2f6a
equal deleted inserted replaced
65082:2e99c0ee3bac 65083:9a0e34edfad1
   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