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