src/Pure/GUI/gui.scala
changeset 69343 395c4fb15ea2
parent 69113 0012f3a08f42
child 69355 cdc2de88d657
--- a/src/Pure/GUI/gui.scala	Sat Nov 24 16:41:18 2018 +0100
+++ b/src/Pure/GUI/gui.scala	Sat Nov 24 18:56:44 2018 +0100
@@ -236,7 +236,7 @@
     font.deriveFont(Map(TextAttribute.TRANSFORM -> new TransformAttribute(transform)))
   }
 
-  def font(family: String = "IsabelleText", size: Int = 1, bold: Boolean = false): Font =
+  def font(family: String = "Isabelle DejaVu Sans", size: Int = 1, bold: Boolean = false): Font =
     new Font(family, if (bold) Font.BOLD else Font.PLAIN, size)
 
   def install_fonts()