more explicit Isabelle_Fonts.Entry;
more robust font embedding into PDF and HTML;
--- 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 + ")")),
--- 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 */
--- 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))
}
}
--- 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
}
--- 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 =>
--- 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)
}
--- 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")
}
--- 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)
}
}