src/Pure/GUI/gui.scala
changeset 69343 395c4fb15ea2
parent 69113 0012f3a08f42
child 69355 cdc2de88d657
equal deleted inserted replaced
69342:fa981730b964 69343:395c4fb15ea2
   234   {
   234   {
   235     import scala.collection.JavaConversions._
   235     import scala.collection.JavaConversions._
   236     font.deriveFont(Map(TextAttribute.TRANSFORM -> new TransformAttribute(transform)))
   236     font.deriveFont(Map(TextAttribute.TRANSFORM -> new TransformAttribute(transform)))
   237   }
   237   }
   238 
   238 
   239   def font(family: String = "IsabelleText", size: Int = 1, bold: Boolean = false): Font =
   239   def font(family: String = "Isabelle DejaVu Sans", size: Int = 1, bold: Boolean = false): Font =
   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()