--- 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
--- 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
--- 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 ***
--- 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)
})
}
--- 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"