# HG changeset patch # User wenzelm # Date 1669386543 -3600 # Node ID d0910be11f655e0653ddf4d846a1d5de1da5c464 # Parent 2bf13b30b98e84f493d694860c1a6b0ff1d39c10 more standard component build process; diff -r 2bf13b30b98e -r d0910be11f65 src/Pure/Admin/build_fonts.scala --- a/src/Pure/Admin/build_fonts.scala Fri Nov 25 14:44:22 2022 +0100 +++ b/src/Pure/Admin/build_fonts.scala Fri Nov 25 15:29:03 2022 +0100 @@ -185,7 +185,7 @@ File.bash_path(source) + " " + File.bash_path(target)).check } - private def hinted_path(hinted: Boolean): Path = + private def make_path(hinted: Boolean = false): Path = if (hinted) Path.basic("ttf-hinted") else Path.basic("ttf") private val hinting = List(false, true) @@ -207,20 +207,26 @@ val default_sources: List[Family] = List(Family.deja_vu_sans_mono, Family.deja_vu_sans, Family.deja_vu_serif) - val default_target_dir: Path = Path.explode("isabelle_fonts") - def build_fonts( + target_dir: Path = Path.current, + target_prefix: String = "Isabelle", sources: List[Family] = default_sources, source_dirs: List[Path] = Nil, - target_prefix: String = "Isabelle", - target_version: String = "", - target_dir: Path = default_target_dir, progress: Progress = new Progress ): Unit = { Isabelle_System.require_command("ttfautohint") - progress.echo("Directory " + target_dir) - hinting.foreach(hinted => Isabelle_System.make_directory(target_dir + hinted_path(hinted))) + + /* component */ + + val component_date = Date.Format.alt_date(Date.now()) + val component_name = "isabelle_fonts-" + component_date + val component_dir = + Components.Directory.create(target_dir + Path.basic(component_name), progress = progress) + + for (hinted <- hinting) { + Isabelle_System.make_directory(component_dir.path + make_path(hinted = 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) @@ -228,7 +234,7 @@ // Isabelle fonts - val targets = + val fonts = for { source <- sources; (source_font, index) <- source.fonts.zipWithIndex } yield { val isabelle_file = find_file(font_dirs, Family.isabelle_symbols.get(index)) @@ -236,12 +242,12 @@ 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 font_names = source_names.update(prefix = target_prefix, version = component_date) Isabelle_System.with_tmp_file("font", "ttf") { tmp_file => for (hinted <- hinting) { - val target_file = target_dir + hinted_path(hinted) + target_names.ttf - progress.echo("Font " + target_file.toString + " ...") + val font_file = component_dir.path + make_path(hinted = hinted) + font_names.ttf + progress.echo("Font " + font_file + " ...") if (hinted) auto_hint(source_file, tmp_file) else Isabelle_System.copy_file(source_file, tmp_file) @@ -260,14 +266,14 @@ Fontforge.select(Range.isabelle_font), Fontforge.paste, - target_names.set, - Fontforge.generate(target_file), + font_names.set, + Fontforge.generate(font_file), Fontforge.close) ).check } } - (target_names.ttf, index) + (font_names.ttf, index) } @@ -276,14 +282,15 @@ { val vacuous_file = find_file(font_dirs, Family.vacuous.get(0)) - val target_names = Fontforge.font_names(vacuous_file) - val target_file = target_dir + hinted_path(false) + target_names.ttf + val font_dir = component_dir.path + make_path() + val font_names = Fontforge.font_names(vacuous_file) + val font_file = font_dir + font_names.ttf - progress.echo("Font " + target_file.toString + " ...") + progress.echo("Font " + font_file + " ...") val domain = - (for ((name, index) <- targets if index == 0) - yield Fontforge.font_domain(target_dir + hinted_path(false) + name)) + (for ((name, index) <- fonts if index == 0) + yield Fontforge.font_domain(font_dir + name)) .flatten.distinct.sorted Fontforge.execute( @@ -299,37 +306,35 @@ .mkString("\n", "\n", "\n") + Fontforge.commands( - Fontforge.generate(target_file), + Fontforge.generate(font_file), Fontforge.close) ).check } - // etc/settings - - val settings_path = Components.Directory(target_dir).settings - Isabelle_System.make_directory(settings_path.dir) + /* settings */ - def fonts_settings(hinted: Boolean): String = + def make_settings(hinted: Boolean = false): String = "\n isabelle_fonts \\\n" + - (for ((target, _) <- targets) yield - """ "$COMPONENT/""" + hinted_path(hinted).file_name + "/" + target.file_name + "\"") + (for ((ttf, _) <- fonts) yield + """ "$COMPONENT/""" + make_path(hinted = hinted).file_name + "/" + ttf.file_name + "\"") .mkString(" \\\n") - File.write(settings_path, + File.write(component_dir.settings, """# -*- shell-script -*- :mode=shellscript: if grep "isabelle_fonts_hinted.*=.*false" "$ISABELLE_HOME_USER/etc/preferences" >/dev/null 2>/dev/null -then""" + fonts_settings(false) + """ -else""" + fonts_settings(true) + """ +then""" + make_settings() + """ +else""" + make_settings(hinted = true) + """ fi -isabelle_fonts_hidden "$COMPONENT/""" + hinted_path(false).file_name + """/Vacuous.ttf" +isabelle_fonts_hidden "$COMPONENT/""" + make_path().file_name + """/Vacuous.ttf" """) - // README - Isabelle_System.copy_file(Path.explode("~~/Admin/isabelle_fonts/README"), target_dir) + /* README */ + + Isabelle_System.copy_file(Path.explode("~~/Admin/isabelle_fonts/README"), component_dir.README) } @@ -338,27 +343,26 @@ val isabelle_tool = Isabelle_Tool("build_fonts", "construct Isabelle fonts", Scala_Project.here, { args => + var target_dir = Path.current var source_dirs: List[Path] = Nil val getopts = Getopts(""" Usage: isabelle build_fonts [OPTIONS] Options are: + -D DIR target directory (default ".") -d DIR additional source directory Construct Isabelle fonts from DejaVu font families and Isabelle symbols. """, + "D:" -> (arg => target_dir = Path.explode(arg)), "d:" -> (arg => source_dirs = source_dirs ::: List(Path.explode(arg)))) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() - val target_version = Date.Format.alt_date(Date.now()) - val target_dir = Path.explode("isabelle_fonts-" + target_version) - val progress = new Console_Progress - build_fonts(source_dirs = source_dirs, target_dir = target_dir, - target_version = target_version, progress = progress) + build_fonts(target_dir = target_dir, source_dirs = source_dirs, progress = progress) }) }