# HG changeset patch # User wenzelm # Date 1554581125 -7200 # Node ID 54dc580863511c0fe5ae0f749d7c751324808be9 # Parent 9a03e9d5f33691d00047ef742502d4d978242c28 support both hinted and unhinted fonts; diff -r 9a03e9d5f336 -r 54dc58086351 Admin/components/components.sha1 --- a/Admin/components/components.sha1 Fri Apr 05 23:45:35 2019 +0200 +++ b/Admin/components/components.sha1 Sat Apr 06 22:05:25 2019 +0200 @@ -81,6 +81,7 @@ f249bc2c85bd2af9eee509de17187a766b74ab86 isabelle_fonts-20181129.tar.gz 928b5320073d04d93bcc5bc4347b6d01632b9d45 isabelle_fonts-20190210.tar.gz dfcdf9a757b9dc36cee87f82533b43c58ba84abe isabelle_fonts-20190309.tar.gz +95e3acf038df7fdeeacd8b4769930e6f57bf3692 isabelle_fonts-20190406.tar.gz 0b2206f914336dec4923dd0479d8cee4b904f544 jdk-11+28.tar.gz 3e05213cad47dbef52804fe329395db9b4e57f39 jdk-11.0.2+9.tar.gz 71d19df63816e9be1c4c5eb44aea7a44cfadb319 jdk-11.tar.gz diff -r 9a03e9d5f336 -r 54dc58086351 Admin/components/main --- a/Admin/components/main Fri Apr 05 23:45:35 2019 +0200 +++ b/Admin/components/main Sat Apr 06 22:05:25 2019 +0200 @@ -4,7 +4,7 @@ csdp-6.x cvc4-1.5-4 e-2.0-2 -isabelle_fonts-20190309 +isabelle_fonts-20190406 jdk-11.0.2+9 jedit_build-20190224 jfreechart-1.5.0 diff -r 9a03e9d5f336 -r 54dc58086351 NEWS --- a/NEWS Fri Apr 05 23:45:35 2019 +0200 +++ b/NEWS Sat Apr 06 22:05:25 2019 +0200 @@ -90,10 +90,16 @@ storage directory for "isabelle build". Option "-n" is now clearly separated from option "-s". +* Isabelle DejaVu fonts are available with hinting by default, which is +relevant for low-resolution displays. This may be disabled via system +option "isabelle_fonts_hinted = false" in +$ISABELLE_HOME_USER/etc/settings -- it occasionally yields better +results. + * OpenJDK 11 has quite different font rendering, with better glyph shapes and improved sub-pixel anti-aliasing. In some situations results -might be *worse* than Oracle Java 8, though. A decent HiDPI display is -recommended. +might be *worse* than Oracle Java 8, though -- a proper HiDPI / UHD +display is recommended. *** Document preparation *** diff -r 9a03e9d5f336 -r 54dc58086351 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) }) } diff -r 9a03e9d5f336 -r 54dc58086351 src/Tools/jEdit/etc/options --- a/src/Tools/jEdit/etc/options Fri Apr 05 23:45:35 2019 +0200 +++ b/src/Tools/jEdit/etc/options Sat Apr 06 22:05:25 2019 +0200 @@ -39,6 +39,9 @@ public option jedit_text_overview : bool = true -- "paint text overview column" +public option isabelle_fonts_hinted : bool = true + -- "use hinted Isabelle DejaVu fonts (change requires restart)" + section "Indentation"