src/Pure/Admin/build_fonts.scala
author wenzelm
Sun Feb 10 18:12:24 2019 +0100 (5 months ago ago)
changeset 69975 04c50000fad1
parent 69974 4791988fcbc4
child 70066 6dc5506ad449
permissions -rw-r--r--
recovered missing glyph;
     1 /*  Title:      Pure/Admin/build_fonts.scala
     2     Author:     Makarius
     3 
     4 Build standard Isabelle fonts: DejaVu base + Isabelle symbols.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 object Build_Fonts
    11 {
    12   /* relevant codepoint ranges */
    13 
    14   object Range
    15   {
    16     def base_font: Seq[Int] =
    17       (0x0020 to 0x007e) ++  // ASCII
    18       (0x00a0 to 0x024f) ++  // Latin Extended-A/B
    19       (0x0400 to 0x04ff) ++  // Cyrillic
    20       (0x0600 to 0x06ff) ++  // Arabic
    21       Seq(
    22         0x02dd,  // hungarumlaut
    23         0x2018,  // single quote
    24         0x2019,  // single quote
    25         0x201a,  // single quote
    26         0x201c,  // double quote
    27         0x201d,  // double quote
    28         0x201e,  // double quote
    29         0x2039,  // single guillemet
    30         0x203a,  // single guillemet
    31         0x204b,  // FOOTNOTE
    32         0x20ac,  // Euro
    33         0xfb01,  // ligature fi
    34         0xfb02,  // ligature fl
    35         0xfffd,  // replacement character
    36       )
    37 
    38     def isabelle_font: Seq[Int] =
    39       Seq(
    40         0x05,  // X
    41         0x06,  // Y
    42         0x07,  // EOF
    43         0x7f,  // DEL
    44         0xaf,  // INVERSE
    45         0xac,  // logicalnot
    46         0xb0,  // degree
    47         0xb1,  // plusminus
    48         0xb7,  // periodcentered
    49         0xd7,  // multiply
    50         0xf7,  // divide
    51       ) ++
    52       (0x0370 to 0x03ff) ++  // Greek (pseudo math)
    53       (0x0590 to 0x05ff) ++  // Hebrew (non-mono)
    54       Seq(
    55         0x2010,  // hyphen
    56         0x2013,  // dash
    57         0x2014,  // dash
    58         0x2015,  // dash
    59         0x2020,  // dagger
    60         0x2021,  // double dagger
    61         0x2022,  // bullet
    62         0x2026,  // ellipsis
    63         0x2030,  // perthousand
    64         0x2032,  // minute
    65         0x2033,  // second
    66         0x2038,  // caret
    67         0x20cd,  // currency symbol
    68       ) ++
    69       (0x2100 to 0x214f) ++  // Letterlike Symbols
    70       (0x2190 to 0x21ff) ++  // Arrows
    71       (0x2200 to 0x22ff) ++  // Mathematical Operators
    72       (0x2300 to 0x23ff) ++  // Miscellaneous Technical
    73       Seq(
    74         0x2423,  // graphic for space
    75         0x2500,  // box drawing
    76         0x2501,  // box drawing
    77         0x2508,  // box drawing
    78         0x2509,  // box drawing
    79         0x2550,  // box drawing
    80       ) ++
    81       (0x25a0 to 0x25ff) ++  // Geometric Shapes
    82       Seq(
    83         0x261b,  // ACTION
    84         0x2660,  // spade suit
    85         0x2661,  // heart suit
    86         0x2662,  // diamond suit
    87         0x2663,  // club suit
    88         0x266d,  // musical flat
    89         0x266e,  // musical natural
    90         0x266f,  // musical sharp
    91         0x2756,  // UNDEFINED
    92         0x2759,  // BOLD
    93         0x27a7,  // DESCR
    94         0x27e6,  // left white square bracket
    95         0x27e7,  // right white square bracket
    96         0x27e8,  // left angle bracket
    97         0x27e9,  // right angle bracket
    98       ) ++
    99       (0x27f0 to 0x27ff) ++  // Supplemental Arrows-A
   100       (0x2900 to 0x297f) ++  // Supplemental Arrows-B
   101       (0x2980 to 0x29ff) ++  // Miscellaneous Mathematical Symbols-B
   102       (0x2a00 to 0x2aff) ++  // Supplemental Mathematical Operators
   103       Seq(0x2b1a) ++  // VERBATIM
   104       (0x1d400 to 0x1d7ff) ++  // Mathematical Alphanumeric Symbols
   105       Seq(
   106         0x1f310,  // globe with meridians (Symbola font)
   107         0x1f4d3,  // notebook (Symbola font)
   108         0x1f5c0,  // folder (Symbola font)
   109         0x1f5cf,  // page (Symbola font)
   110       )
   111 
   112     def isabelle_math_font: Seq[Int] =
   113       (0x21 to 0x2f) ++  // bang .. slash
   114       (0x3a to 0x40) ++  // colon .. atsign
   115       (0x5b to 0x5f) ++  // leftbracket .. underscore
   116       (0x7b to 0x7e) ++  // leftbrace .. tilde
   117       Seq(
   118         0xa9,  // copyright
   119         0xae,  // registered
   120       )
   121 
   122     val vacuous_font: Seq[Int] =
   123       Seq(0x3c)  // "<" as template
   124   }
   125 
   126 
   127   /* font families */
   128 
   129   sealed case class Family(
   130     plain: String = "",
   131     bold: String = "",
   132     italic: String = "",
   133     bold_italic: String = "")
   134   {
   135     val fonts: List[String] =
   136       proper_string(plain).toList :::
   137       proper_string(bold).toList :::
   138       proper_string(italic).toList :::
   139       proper_string(bold_italic).toList
   140 
   141     def get(index: Int): String = fonts(index % fonts.length)
   142   }
   143 
   144   object Family
   145   {
   146     def isabelle_symbols: Family =
   147       Family(
   148         plain = "IsabelleSymbols.sfd",
   149         bold = "IsabelleSymbolsBold.sfd")
   150 
   151     def deja_vu_sans_mono: Family =
   152       Family(
   153         plain = "DejaVuSansMono.ttf",
   154         bold = "DejaVuSansMono-Bold.ttf",
   155         italic = "DejaVuSansMono-Oblique.ttf",
   156         bold_italic = "DejaVuSansMono-BoldOblique.ttf")
   157 
   158     def deja_vu_sans: Family =
   159       Family(
   160         plain = "DejaVuSans.ttf",
   161         bold = "DejaVuSans-Bold.ttf",
   162         italic = "DejaVuSans-Oblique.ttf",
   163         bold_italic = "DejaVuSans-BoldOblique.ttf")
   164 
   165     def deja_vu_serif: Family =
   166       Family(
   167         plain = "DejaVuSerif.ttf",
   168         bold = "DejaVuSerif-Bold.ttf",
   169         italic = "DejaVuSerif-Italic.ttf",
   170         bold_italic = "DejaVuSerif-BoldItalic.ttf")
   171 
   172     def vacuous: Family = Family(plain = "Vacuous.sfd")
   173   }
   174 
   175 
   176   /* auto-hinting */
   177   // see https://www.freetype.org/ttfautohint/doc/ttfautohint.html
   178 
   179   def auto_hint(source: Path, target: Path)
   180   {
   181     Isabelle_System.bash("ttfautohint -i " +
   182       File.bash_path(source) + " " + File.bash_path(target)).check
   183   }
   184 
   185 
   186 
   187   /* build fonts */
   188 
   189   private def find_file(dirs: List[Path], name: String): Path =
   190   {
   191     val path = Path.explode(name)
   192     dirs.collectFirst({ case dir if (dir + path).is_file => dir + path }) match {
   193       case Some(file) => file
   194       case None =>
   195         error(cat_lines(
   196           ("Failed to find font file " + path + " in directories:") ::
   197             dirs.map(dir => "  " + dir.toString)))
   198     }
   199   }
   200 
   201   val default_sources: List[Family] =
   202     List(Family.deja_vu_sans_mono, Family.deja_vu_sans, Family.deja_vu_serif)
   203 
   204   val default_target_dir: Path = Path.explode("isabelle_fonts")
   205 
   206   def build_fonts(
   207     sources: List[Family] = default_sources,
   208     source_dirs: List[Path] = Nil,
   209     target_prefix: String = "Isabelle",
   210     target_version: String = "",
   211     target_dir: Path = default_target_dir,
   212     progress: Progress = No_Progress)
   213   {
   214     progress.echo("Directory " + target_dir)
   215     Isabelle_System.mkdirs(target_dir)
   216 
   217     val font_dirs = source_dirs ::: List(Path.explode("~~/Admin/isabelle_fonts"))
   218     for (dir <- font_dirs if !dir.is_dir) error("Bad source directory: " + dir)
   219 
   220 
   221     // Isabelle fonts
   222 
   223     val targets =
   224       for { source <- sources; (source_font, index) <- source.fonts.zipWithIndex }
   225       yield {
   226         val isabelle_file = find_file(font_dirs, Family.isabelle_symbols.get(index))
   227 
   228         val source_file = find_file(font_dirs, source_font)
   229         val source_names = Fontforge.font_names(source_file)
   230 
   231         val target_names = source_names.update(prefix = target_prefix, version = target_version)
   232         val target_file = target_dir + target_names.ttf
   233 
   234         progress.echo("Font " + target_file.toString + " ...")
   235         Isabelle_System.with_tmp_file("font", "ttf")(tmp_file =>
   236         {
   237           auto_hint(source_file, tmp_file)
   238 
   239           Fontforge.execute(
   240             Fontforge.commands(
   241               Fontforge.open(isabelle_file),
   242               Fontforge.select(Range.isabelle_font),
   243               Fontforge.copy,
   244               Fontforge.close,
   245 
   246               Fontforge.open(tmp_file),
   247               Fontforge.select(Range.base_font),
   248               Fontforge.select_invert,
   249               Fontforge.clear,
   250               Fontforge.select(Range.isabelle_font),
   251               Fontforge.paste,
   252 
   253               target_names.set,
   254               Fontforge.generate(target_file),
   255               Fontforge.close)
   256           ).check
   257         })
   258 
   259         (target_file, index)
   260       }
   261 
   262 
   263     // Vacuous font
   264 
   265     {
   266       val vacuous_file = find_file(font_dirs, Family.vacuous.get(0))
   267 
   268       val target_names = Fontforge.font_names(vacuous_file)
   269       val target_file = target_dir + target_names.ttf
   270 
   271       progress.echo("Font " + target_file.toString + " ...")
   272 
   273       val domain =
   274         (for ((target_file, index) <- targets if index == 0)
   275           yield Fontforge.font_domain(target_file)).flatten.toSet.toList.sorted
   276 
   277       Fontforge.execute(
   278         Fontforge.commands(
   279           Fontforge.open(vacuous_file),
   280           Fontforge.select(Range.vacuous_font),
   281           Fontforge.copy) +
   282 
   283         domain.map(code =>
   284             Fontforge.commands(
   285               Fontforge.select(Seq(code)),
   286               Fontforge.paste))
   287           .mkString("\n", "\n", "\n") +
   288 
   289         Fontforge.commands(
   290           Fontforge.generate(target_file),
   291           Fontforge.close)
   292       ).check
   293     }
   294 
   295 
   296     // etc/settings
   297 
   298     val settings_path = Components.settings(target_dir)
   299     Isabelle_System.mkdirs(settings_path.dir)
   300     File.write(settings_path,
   301       "# -*- shell-script -*- :mode=shellscript:\n\nisabelle_fonts \\\n" +
   302       (for ((path, _) <- targets)
   303         yield """  "$COMPONENT/""" + path.file_name + "\"").mkString(" \\\n") +
   304       """
   305 
   306 isabelle_fonts_hidden "$COMPONENT/Vacuous.ttf"
   307 """)
   308 
   309 
   310     // README
   311     File.copy(Path.explode("~~/Admin/isabelle_fonts/README"), target_dir)
   312   }
   313 
   314 
   315   /* Isabelle tool wrapper */
   316 
   317   val isabelle_tool =
   318     Isabelle_Tool("build_fonts", "construct Isabelle fonts", args =>
   319     {
   320       var source_dirs: List[Path] = Nil
   321 
   322       val getopts = Getopts("""
   323 Usage: isabelle build_fonts [OPTIONS]
   324 
   325   Options are:
   326     -d DIR       additional source directory
   327 
   328   Construct Isabelle fonts from DejaVu font families and Isabelle symbols.
   329 """,
   330         "d:" -> (arg => source_dirs = source_dirs ::: List(Path.explode(arg))))
   331 
   332       val more_args = getopts(args)
   333       if (more_args.nonEmpty) getopts.usage()
   334 
   335       val target_version = Date.Format("uuuuMMdd")(Date.now())
   336       val target_dir = Path.explode("isabelle_fonts-" + target_version)
   337 
   338       val progress = new Console_Progress
   339 
   340       build_fonts(source_dirs = source_dirs, target_dir = target_dir,
   341         target_version = target_version, progress = progress)
   342     })
   343 }