src/Pure/General/graphics_file.scala
changeset 69360 dc9a39c3f75d
parent 69355 cdc2de88d657
child 69365 c5b3860d29ef
--- a/src/Pure/General/graphics_file.scala	Wed Nov 28 13:59:29 2018 +0100
+++ b/src/Pure/General/graphics_file.scala	Wed Nov 28 14:00:22 2018 +0100
@@ -44,13 +44,11 @@
   private def font_mapper(): FontMapper =
   {
     val mapper = new DefaultFontMapper
-    for {
-      font <- Isabelle_Fonts.files()
-      name <- Library.try_unsuffix(".ttf", font.base_name)
-    } {
-      val parameters = new DefaultFontMapper.BaseFontParameters(File.platform_path(font))
-      parameters.encoding = BaseFont.IDENTITY_H
-      mapper.putName(name, parameters)
+    for (entry <- Isabelle_Fonts.fonts()) {
+      val params = new DefaultFontMapper.BaseFontParameters(File.platform_path(entry.path))
+      params.encoding = BaseFont.IDENTITY_H
+      params.embedded = true
+      mapper.putName(entry.name, params)
     }
     mapper
   }