diff -r 3b709d9074ec -r dc9a39c3f75d src/Pure/System/isabelle_fonts.scala
--- a/src/Pure/System/isabelle_fonts.scala	Wed Nov 28 13:59:29 2018 +0100
+++ b/src/Pure/System/isabelle_fonts.scala	Wed Nov 28 14:00:22 2018 +0100
@@ -8,6 +8,9 @@
 package isabelle
 
 
+import java.awt.Font
+
+
 object Isabelle_Fonts
 {
   /* standard names */
@@ -17,18 +20,34 @@
   val serif: String = "Isabelle DejaVu Serif"
 
 
-  /* Isabelle system environment */
+  /* environment entries */
 
-  def variables(html: Boolean = false): List[String] =
-    if (html) List("ISABELLE_FONTS", "ISABELLE_FONTS_HTML") else List("ISABELLE_FONTS")
+  sealed case class Entry(path: Path, html: Boolean = false)
+  {
+    def bytes: Bytes = Bytes.read(path)
+
+    lazy val font: Font = Font.createFont(Font.TRUETYPE_FONT, path.file)
+    def family: String = font.getFamily
+    def name: String = font.getFontName
 
-  def files(
-    html: Boolean = false,
-    getenv: String => String = Isabelle_System.getenv_strict(_)): List[Path] =
+    // educated guessing
+    private lazy val name_lowercase = Word.lowercase(name)
+    def is_bold: Boolean =
+      name_lowercase.containsSlice("bold")
+    def is_italic: Boolean =
+      name_lowercase.containsSlice("italic") || name_lowercase.containsSlice("oblique")
+  }
+
+  def make_entries(
+    getenv: String => String = Isabelle_System.getenv_strict(_),
+    html: Boolean = false): List[Entry] =
   {
-    for {
-      variable <- variables(html = html)
-      path <- Path.split(getenv(variable))
-    } yield path
+    Path.split(getenv("ISABELLE_FONTS")).map(Entry(_)) :::
+    (if (html) Path.split(getenv("ISABELLE_FONTS_HTML")).map(Entry(_, html = true)) else Nil)
   }
+
+  private lazy val all_fonts: List[Entry] = make_entries(html = true)
+
+  def fonts(html: Boolean = false): List[Entry] =
+    if (html) all_fonts else all_fonts.filter(entry => !entry.html)
 }