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