src/Pure/Admin/build_fonts.scala

--- a/src/Pure/Admin/build_fonts.scala	Fri Apr 05 23:45:35 2019 +0200
+++ b/src/Pure/Admin/build_fonts.scala	Sat Apr 06 22:05:25 2019 +0200
@@ -174,15 +174,19 @@
   }
 
 
-  /* auto-hinting */
+  /* hinting */
+
   // see https://www.freetype.org/ttfautohint/doc/ttfautohint.html
-
-  def auto_hint(source: Path, target: Path)
+  private def auto_hint(source: Path, target: Path)
   {
     Isabelle_System.bash("ttfautohint -i " +
       File.bash_path(source) + " " + File.bash_path(target)).check
   }
 
+  private def hinted_path(hinted: Boolean): Path =
+    if (hinted) Path.basic("ttf-hinted") else Path.basic("ttf")
+
+  private val hinting = List(false, true)
 
 
   /* build fonts */
@@ -210,11 +214,10 @@
     target_prefix: String = "Isabelle",
     target_version: String = "",
     target_dir: Path = default_target_dir,
-    unhinted: Boolean = false,
     progress: Progress = No_Progress)
   {
     progress.echo("Directory " + target_dir)
-    Isabelle_System.mkdirs(target_dir)
+    hinting.foreach(hinted => Isabelle_System.mkdirs(target_dir + hinted_path(hinted)))
 
     val font_dirs = source_dirs ::: List(Path.explode("~~/Admin/isabelle_fonts"))
     for (dir <- font_dirs if !dir.is_dir) error("Bad source directory: " + dir)
@@ -231,35 +234,38 @@
         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("Font " + target_file.toString + " ...")
         Isabelle_System.with_tmp_file("font", "ttf")(tmp_file =>
         {
-          if (unhinted) File.copy(source_file, tmp_file)
-          else auto_hint(source_file, tmp_file)
+          for (hinted <- hinting) {
+            val target_file = target_dir + hinted_path(hinted) + target_names.ttf
+            progress.echo("Font " + target_file.toString + " ...")
 
-          Fontforge.execute(
-            Fontforge.commands(
-              Fontforge.open(isabelle_file),
-              Fontforge.select(Range.isabelle_font),
-              Fontforge.copy,
-              Fontforge.close,
+            if (hinted) auto_hint(source_file, tmp_file)
+            else File.copy(source_file, tmp_file)
 
-              Fontforge.open(tmp_file),
-              Fontforge.select(Range.base_font),
-              Fontforge.select_invert,
-              Fontforge.clear,
-              Fontforge.select(Range.isabelle_font),
-              Fontforge.paste,
+            Fontforge.execute(
+              Fontforge.commands(
+                Fontforge.open(isabelle_file),
+                Fontforge.select(Range.isabelle_font),
+                Fontforge.copy,
+                Fontforge.close,
 
-              target_names.set,
-              Fontforge.generate(target_file),
-              Fontforge.close)
-          ).check
+                Fontforge.open(tmp_file),
+                Fontforge.select(Range.base_font),
+                Fontforge.select_invert,
+                Fontforge.clear,
+                Fontforge.select(Range.isabelle_font),
+                Fontforge.paste,
+
+                target_names.set,
+                Fontforge.generate(target_file),
+                Fontforge.close)
+            ).check
+          }
         })
 
-        (target_file, index)
+        (target_names.ttf, index)
       }
 
 
@@ -269,13 +275,14 @@
       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
+      val target_file = target_dir + hinted_path(false) + target_names.ttf
 
       progress.echo("Font " + target_file.toString + " ...")
 
       val domain =
-        (for ((target_file, index) <- targets if index == 0)
-          yield Fontforge.font_domain(target_file)).flatten.toSet.toList.sorted
+        (for ((name, index) <- targets if index == 0)
+          yield Fontforge.font_domain(target_dir + hinted_path(false) + name))
+        .flatten.toSet.toList.sorted
 
       Fontforge.execute(
         Fontforge.commands(
@@ -300,13 +307,22 @@
 
     val settings_path = Components.settings(target_dir)
     Isabelle_System.mkdirs(settings_path.dir)
+
+    def fonts_settings(hinted: Boolean): String =
+      "\n  isabelle_fonts \\\n" +
+      (for ((target, _) <- targets) yield
+        """    "$COMPONENT/""" + hinted_path(hinted).file_name + "/" + target.file_name + "\"")
+      .mkString(" \\\n")
+
     File.write(settings_path,
-      "# -*- shell-script -*- :mode=shellscript:\n\nisabelle_fonts \\\n" +
-      (for ((path, _) <- targets)
-        yield """  "$COMPONENT/""" + path.file_name + "\"").mkString(" \\\n") +
-      """
+      """# -*- shell-script -*- :mode=shellscript:
 
-isabelle_fonts_hidden "$COMPONENT/Vacuous.ttf"
+if grep "isabelle_fonts_hinted.*=.*true" "$ISABELLE_HOME_USER/etc/preferences" >/dev/null 2>/dev/null
+then""" + fonts_settings(true) + """
+else""" + fonts_settings(false) + """
+fi
+
+isabelle_fonts_hidden "$COMPONENT/""" + hinted_path(false).file_name + """/Vacuous.ttf"
 """)
 
 
@@ -321,19 +337,16 @@
     Isabelle_Tool("build_fonts", "construct Isabelle fonts", args =>
     {
       var source_dirs: List[Path] = Nil
-      var unhinted = false
 
       val getopts = Getopts("""
 Usage: isabelle build_fonts [OPTIONS]
 
   Options are:
     -d DIR       additional source directory
-    -u           unhinted font (bypass ttfautohint)
 
   Construct Isabelle fonts from DejaVu font families and Isabelle symbols.
 """,
-        "d:" -> (arg => source_dirs = source_dirs ::: List(Path.explode(arg))),
-        "u" -> (_ => unhinted = true))
+        "d:" -> (arg => source_dirs = source_dirs ::: List(Path.explode(arg))))
 
       val more_args = getopts(args)
       if (more_args.nonEmpty) getopts.usage()
@@ -344,6 +357,6 @@
       val progress = new Console_Progress
 
       build_fonts(source_dirs = source_dirs, target_dir = target_dir,
-        target_version = target_version, unhinted = unhinted, progress = progress)
+        target_version = target_version, progress = progress)
     })
 }