# HG changeset patch
# User wenzelm
# Date 1543410022 -3600
# Node ID dc9a39c3f75dd2b69f7cb6d6cb841655b5952a87
# Parent  3b709d9074ec8d13acdb8a097ed6591c49db9ab9
more explicit Isabelle_Fonts.Entry;
more robust font embedding into PDF and HTML;

diff -r 3b709d9074ec -r dc9a39c3f75d src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Wed Nov 28 13:59:29 2018 +0100
+++ b/src/Pure/Admin/build_release.scala	Wed Nov 28 14:00:22 2018 +0100
@@ -116,9 +116,7 @@
     val target = other_isabelle.isabelle_home + Path.explode("doc")
     val target_fonts = target + Path.explode("fonts")
     Isabelle_System.mkdirs(target_fonts)
-
-    for (font <- other_isabelle.fonts(html = true))
-      File.copy(font, target_fonts)
+    other_isabelle.copy_fonts(target_fonts)
 
     HTML.write_document(target, "NEWS.html",
       List(HTML.title("NEWS (" + dist_version + ")")),
diff -r 3b709d9074ec -r dc9a39c3f75d src/Pure/Admin/other_isabelle.scala
--- a/src/Pure/Admin/other_isabelle.scala	Wed Nov 28 13:59:29 2018 +0100
+++ b/src/Pure/Admin/other_isabelle.scala	Wed Nov 28 14:00:22 2018 +0100
@@ -61,8 +61,9 @@
   val etc_settings: Path = etc + Path.explode("settings")
   val etc_preferences: Path = etc + Path.explode("preferences")
 
-  def fonts(html: Boolean = false): List[Path] =
-    Isabelle_Fonts.files(html = html, getenv = getenv(_))
+  def copy_fonts(target_dir: Path): Unit =
+    Isabelle_Fonts.make_entries(getenv = getenv(_), html = true).
+      foreach(entry => File.copy(entry.path, target_dir))
 
 
   /* settings */
diff -r 3b709d9074ec -r dc9a39c3f75d src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Wed Nov 28 13:59:29 2018 +0100
+++ b/src/Pure/GUI/gui.scala	Wed Nov 28 14:00:22 2018 +0100
@@ -246,8 +246,7 @@
   def install_fonts()
   {
     val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
-    for (path <- Isabelle_Fonts.files())
-      ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, path.file))
+    Isabelle_Fonts.fonts().foreach(entry => ge.registerFont(entry.font))
   }
 }
 
diff -r 3b709d9074ec -r dc9a39c3f75d src/Pure/General/graphics_file.scala
--- 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
   }
diff -r 3b709d9074ec -r dc9a39c3f75d src/Pure/General/http.scala
--- a/src/Pure/General/http.scala	Wed Nov 28 13:59:29 2018 +0100
+++ b/src/Pure/General/http.scala	Wed Nov 28 14:00:22 2018 +0100
@@ -155,8 +155,7 @@
   /* fonts */
 
   private lazy val html_fonts: SortedMap[String, Bytes] =
-    SortedMap(
-      Isabelle_Fonts.files(html = true).map(path => (path.base_name -> Bytes.read(path))): _*)
+    SortedMap(Isabelle_Fonts.fonts(html = true).map(entry => (entry.name -> entry.bytes)): _*)
 
   def fonts(root: String = "/fonts"): Handler =
     get(root, arg =>
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)
 }
diff -r 3b709d9074ec -r dc9a39c3f75d src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Wed Nov 28 13:59:29 2018 +0100
+++ b/src/Pure/Thy/html.scala	Wed Nov 28 14:00:22 2018 +0100
@@ -350,40 +350,25 @@
   /* fonts */
 
   def fonts_url(): String => String =
-    (for (path <- Isabelle_Fonts.files(html = true))
-     yield (path.base_name -> Url.print_file(path.file))).toMap
+    (for (entry <- Isabelle_Fonts.fonts(html = true))
+     yield (entry.name -> Url.print_file(entry.path.file))).toMap
 
   def fonts_dir(prefix: String)(ttf_name: String): String =
     prefix + "/" + ttf_name
 
   def fonts_css(make_url: String => String = fonts_url()): String =
   {
-    def font_face(
-        name: String, ttf_name: String, bold: Boolean = false, italic: Boolean = false): String =
+    def font_face(entry: Isabelle_Fonts.Entry): String =
       cat_lines(
         List(
           "@font-face {",
-          "  font-family: '" + name + "';",
-          "  src: url('" + make_url(ttf_name) + "') format('truetype');") :::
-        (if (bold) List("  font-weight: bold;") else Nil) :::
-        (if (italic) List("  font-style: italic;") else Nil) :::
+          "  font-family: '" + entry.family + "';",
+          "  src: url('" + make_url(entry.path.base_name) + "') format('truetype');") :::
+        (if (entry.is_bold) List("  font-weight: bold;") else Nil) :::
+        (if (entry.is_italic) List("  font-style: italic;") else Nil) :::
         List("}"))
 
-    List(
-      "/* Isabelle fonts */",
-      font_face("Isabelle DejaVu Sans Mono", "IsabelleDejaVuSansMono.ttf"),
-      font_face("Isabelle DejaVu Sans Mono", "IsabelleDejaVuSansMono-Bold.ttf", bold = true),
-      font_face("Isabelle DejaVu Sans Mono", "IsabelleDejaVuSansMono-Oblique.ttf", italic = true),
-      font_face("Isabelle DejaVu Sans Mono", "IsabelleDejaVuSansMono-BoldOblique.ttf", bold = true, italic = true),
-      font_face("Isabelle DejaVu Sans", "IsabelleDejaVuSans.ttf"),
-      font_face("Isabelle DejaVu Sans", "IsabelleDejaVuSans-Bold.ttf", bold = true),
-      font_face("Isabelle DejaVu Sans", "IsabelleDejaVuSans-Oblique.ttf", italic = true),
-      font_face("Isabelle DejaVu Sans", "IsabelleDejaVuSans-BoldOblique.ttf", bold = true, italic = true),
-      font_face("Isabelle DejaVu Serif", "IsabelleDejaVuSerif.ttf"),
-      font_face("Isabelle DejaVu Serif", "IsabelleDejaVuSerif-Bold.ttf", bold = true),
-      font_face("Isabelle DejaVu Serif", "IsabelleDejaVuSerif-Italic.ttf", italic = true),
-      font_face("Isabelle DejaVu Serif", "IsabelleDejaVuSerif-BoldItalic.ttf", bold = true, italic = true),
-      font_face("Vacuous", "Vacuous.ttf")).mkString("\n\n")
+    ("/* Isabelle fonts */" :: Isabelle_Fonts.fonts(html = true).map(font_face(_))).mkString("\n\n")
   }
 
 
diff -r 3b709d9074ec -r dc9a39c3f75d src/Pure/Thy/present.scala
--- a/src/Pure/Thy/present.scala	Wed Nov 28 13:59:29 2018 +0100
+++ b/src/Pure/Thy/present.scala	Wed Nov 28 14:00:22 2018 +0100
@@ -96,8 +96,8 @@
 
       HTML.write_isabelle_css(session_prefix)
 
-      for (path <- Isabelle_Fonts.files(html = true))
-        File.copy(path, session_fonts)
+      for (entry <- Isabelle_Fonts.fonts(html = true))
+        File.copy(entry.path, session_fonts)
     }
   }