# HG changeset patch
# User wenzelm
# Date 1543491791 -3600
# Node ID 3539767d5c6102180908f19b07ab125592492a8a
# Parent  589896fe1df2efd0bc3f154dfcd33c9af51aa2db
generate Vacuous font from domain of Isabelle fonts;

diff -r 589896fe1df2 -r 3539767d5c61 src/Pure/Admin/build_fonts.scala
--- a/src/Pure/Admin/build_fonts.scala	Thu Nov 29 12:41:53 2018 +0100
+++ b/src/Pure/Admin/build_fonts.scala	Thu Nov 29 12:43:11 2018 +0100
@@ -107,6 +107,9 @@
         0x1f5c0,  // folder (Symbola font)
         0x1f5cf,  // page (Symbola font)
       )
+
+      val vacuous_font: Seq[Int] =
+        Seq(0x3c)  // "<" as template
   }
 
 
@@ -154,6 +157,8 @@
         bold = "DejaVuSerif-Bold.ttf",
         italic = "DejaVuSerif-Italic.ttf",
         bold_italic = "DejaVuSerif-BoldItalic.ttf")
+
+    def vacuous: Family = Family(plain = "Vacuous.sfd")
   }
 
 
@@ -187,31 +192,71 @@
     val font_dirs = source_dirs ::: List(Path.explode("~~/Admin/isabelle_fonts"))
     for (dir <- font_dirs if !dir.is_dir) error("Bad source directory: " + dir)
 
-    for { source <- sources; (source_font, index) <- source.fonts.zipWithIndex } {
-      val isabelle_file = find_file(font_dirs, Family.isabelle_text.get(index))
+
+    // Isabelle fonts
+
+    val targets =
+      for { source <- sources; (source_font, index) <- source.fonts.zipWithIndex }
+      yield {
+        val isabelle_file = find_file(font_dirs, Family.isabelle_text.get(index))
+
+        val source_file = find_file(font_dirs, source_font)
+        val source_names = Fontforge.font_names(source_file)
+
+        val target_names = source_names.update(prefix = target_prefix, version = target_version)
+        val target_file = target_dir + target_names.ttf
+
+        progress.echo("Creating " + target_file.toString + " ...")
+        Fontforge.execute(
+          Fontforge.commands(
+            Fontforge.open(isabelle_file),
+            Fontforge.select(Range.isabelle_font),
+            Fontforge.copy,
+            Fontforge.close,
 
-      val source_file = find_file(font_dirs, source_font)
-      val source_names = Fontforge.font_names(source_file)
+            Fontforge.open(source_file),
+            Fontforge.select(Range.base_font),
+            Fontforge.select_invert,
+            Fontforge.clear,
+            Fontforge.select(Range.isabelle_font),
+            Fontforge.paste,
 
-      val target_names = source_names.update(prefix = target_prefix, version = target_version)
+            target_names.set,
+            Fontforge.generate(target_file),
+            Fontforge.close)
+        ).check
+
+        (target_file, index)
+      }
+
+
+    // Vacuous font
+
+    {
+      val vacuous_file = find_file(font_dirs, Family.vacuous.get(0))
+
+      val target_names = Fontforge.font_names(vacuous_file)
       val target_file = target_dir + target_names.ttf
 
       progress.echo("Creating " + target_file.toString + " ...")
+
+      val domain =
+        (for ((target_file, index) <- targets if index == 0)
+          yield Fontforge.font_domain(target_file)).flatten.toSet.toList.sorted
+
       Fontforge.execute(
         Fontforge.commands(
-          Fontforge.open(isabelle_file),
-          Fontforge.select(Range.isabelle_font),
-          Fontforge.copy,
-          Fontforge.close,
+          Fontforge.open(vacuous_file),
+          Fontforge.select(Range.vacuous_font),
+          Fontforge.copy) +
 
-          Fontforge.open(source_file),
-          Fontforge.select(Range.base_font),
-          Fontforge.select_invert,
-          Fontforge.clear,
-          Fontforge.select(Range.isabelle_font),
-          Fontforge.paste,
+        domain.map(code =>
+            Fontforge.commands(
+              Fontforge.select(Seq(code)),
+              Fontforge.paste))
+          .mkString("\n", "\n", "\n") +
 
-          target_names.set,
+        Fontforge.commands(
           Fontforge.generate(target_file),
           Fontforge.close)
       ).check