auto-hinting of original DejaVu fonts, but not Isabelle symbols;

--- a/src/Pure/Admin/build_fonts.scala	Fri Feb 08 14:42:28 2019 +0100
+++ b/src/Pure/Admin/build_fonts.scala	Sun Feb 10 18:04:48 2019 +0100
@@ -172,6 +172,17 @@
   }
 
 
+  /* auto-hinting */
+  // see https://www.freetype.org/ttfautohint/doc/ttfautohint.html
+
+  def auto_hint(source: Path, target: Path)
+  {
+    Isabelle_System.bash("ttfautohint -i " +
+      File.bash_path(source) + " " + File.bash_path(target)).check
+  }
+
+
+
   /* build fonts */
 
   private def find_file(dirs: List[Path], name: String): Path =
@@ -220,24 +231,29 @@
         val target_file = target_dir + 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,
+        Isabelle_System.with_tmp_file("font", "ttf")(tmp_file =>
+        {
+          auto_hint(source_file, tmp_file)
+
+          Fontforge.execute(
+            Fontforge.commands(
+              Fontforge.open(isabelle_file),
+              Fontforge.select(Range.isabelle_font),
+              Fontforge.copy,
+              Fontforge.close,
 
-            Fontforge.open(source_file),
-            Fontforge.select(Range.base_font),
-            Fontforge.select_invert,
-            Fontforge.clear,
-            Fontforge.select(Range.isabelle_font),
-            Fontforge.paste,
+              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_names.set,
+              Fontforge.generate(target_file),
+              Fontforge.close)
+          ).check
+        })
 
         (target_file, index)
       }