# HG changeset patch
# User wenzelm
# Date 1542981032 -3600
# Node ID 85ccc983748ce6c18ccb7ad8635fb95286feafe7
# Parent  85cafb6e4db0dac24482991311b8554e704c2b89
clarified;

diff -r 85cafb6e4db0 -r 85ccc983748c src/Pure/Tools/isabelle_fonts.scala
--- a/src/Pure/Tools/isabelle_fonts.scala	Fri Nov 23 14:30:44 2018 +0100
+++ b/src/Pure/Tools/isabelle_fonts.scala	Fri Nov 23 14:50:32 2018 +0100
@@ -111,29 +111,35 @@
 
   /* font families */
 
-  sealed case class Family(plain: String, bold: String, italic: String, bold_italic: String)
+  sealed case class Family(
+    plain: String = "",
+    bold: String = "",
+    italic: String = "",
+    bold_italic: String = "",
+    fallback: Option[Family] = None)
 
   object Family
   {
-    val deja_vu_sans_mono =
+    def deja_vu_sans_mono: Family =
       Family(
-        "DejaVuSansMono",
-        "DejaVuSansMono-Bold",
-        "DejaVuSansMono-Oblique",
-        "DejaVuSansMono-BoldOblique")
+        plain = "DejaVuSansMono.ttf",
+        bold = "DejaVuSansMono-Bold.ttf",
+        italic = "DejaVuSansMono-Oblique.ttf",
+        bold_italic = "DejaVuSansMono-BoldOblique.ttf",
+        fallback = Some(deja_vu_sans))
 
-    val deja_vu_sans =
+    def deja_vu_sans: Family =
       Family(
-        "DejaVuSans",
-        "DejaVuSans-Bold",
-        "DejaVuSans-Oblique",
-        "DejaVuSans-BoldOblique")
+        plain = "DejaVuSans.ttf",
+        bold = "DejaVuSans-Bold.ttf",
+        italic = "DejaVuSans-Oblique.ttf",
+        bold_italic = "DejaVuSans-BoldOblique.ttf")
 
-    val deja_vu_serif =
+    def deja_vu_serif: Family =
       Family(
-        "DejaVuSerif",
-        "DejaVuSerif-Bold",
-        "DejaVuSerif-Italic",
-        "DejaVuSerif-BoldItalic")
+        plain = "DejaVuSerif.ttf",
+        bold = "DejaVuSerif-Bold.ttf",
+        italic = "DejaVuSerif-Italic.ttf",
+        bold_italic = "DejaVuSerif-BoldItalic.ttf")
   }
 }