--- a/src/Pure/GUI/gui.scala Wed Nov 28 11:41:49 2018 +0100
+++ b/src/Pure/GUI/gui.scala Wed Nov 28 11:43:06 2018 +0100
@@ -236,7 +236,7 @@
font.deriveFont(Map(TextAttribute.TRANSFORM -> new TransformAttribute(transform)))
}
- def font(family: String = "Isabelle DejaVu Sans", size: Int = 1, bold: Boolean = false): Font =
+ def font(family: String = Isabelle_Fonts.sans, size: Int = 1, bold: Boolean = false): Font =
new Font(family, if (bold) Font.BOLD else Font.PLAIN, size)
def install_fonts()
--- a/src/Pure/System/isabelle_fonts.scala Wed Nov 28 11:41:49 2018 +0100
+++ b/src/Pure/System/isabelle_fonts.scala Wed Nov 28 11:43:06 2018 +0100
@@ -10,6 +10,13 @@
object Isabelle_Fonts
{
+ /* standard names */
+
+ val mono: String = "Isabelle DejaVu Sans Mono"
+ val sans: String = "Isabelle DejaVu Sans"
+ val serif: String = "Isabelle DejaVu Serif"
+
+
/* Isabelle system environment */
def variables(html: Boolean = false): List[String] =