1/*  Title:      Pure/Admin/build_fonts.scala
2    Author:     Makarius
3
4Build standard Isabelle fonts: DejaVu base + Isabelle symbols.
5*/
6
7package isabelle
8
9
10object 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        0x27ea,  // left double angle bracket
100        0x27eb,  // right double angle bracket
101      ) ++
102      (0x27f0 to 0x27ff) ++  // Supplemental Arrows-A
103      (0x2900 to 0x297f) ++  // Supplemental Arrows-B
104      (0x2980 to 0x29ff) ++  // Miscellaneous Mathematical Symbols-B
105      (0x2a00 to 0x2aff) ++  // Supplemental Mathematical Operators
106      Seq(0x2b1a) ++  // VERBATIM
107      (0x1d400 to 0x1d7ff) ++  // Mathematical Alphanumeric Symbols
108      Seq(
109        0x1f310,  // globe with meridians (Symbola font)
110        0x1f4d3,  // notebook (Symbola font)
111        0x1f5c0,  // folder (Symbola font)
112        0x1f5cf,  // page (Symbola font)
113      )
114
115    def isabelle_math_font: Seq[Int] =
116      (0x21 to 0x2f) ++  // bang .. slash
117      (0x3a to 0x40) ++  // colon .. atsign
118      (0x5b to 0x5f) ++  // leftbracket .. underscore
119      (0x7b to 0x7e) ++  // leftbrace .. tilde
120      Seq(
121        0xa9,  // copyright
122        0xae,  // registered
123      )
124
125    val vacuous_font: Seq[Int] =
126      Seq(0x3c)  // "<" as template
127  }
128
129
130  /* font families */
131
132  sealed case class Family(
133    plain: String = "",
134    bold: String = "",
135    italic: String = "",
136    bold_italic: String = "")
137  {
138    val fonts: List[String] =
139      proper_string(plain).toList :::
140      proper_string(bold).toList :::
141      proper_string(italic).toList :::
142      proper_string(bold_italic).toList
143
144    def get(index: Int): String = fonts(index % fonts.length)
145  }
146
147  object Family
148  {
149    def isabelle_symbols: Family =
150      Family(
151        plain = "IsabelleSymbols.sfd",
152        bold = "IsabelleSymbolsBold.sfd")
153
154    def deja_vu_sans_mono: Family =
155      Family(
156        plain = "DejaVuSansMono.ttf",
157        bold = "DejaVuSansMono-Bold.ttf",
158        italic = "DejaVuSansMono-Oblique.ttf",
159        bold_italic = "DejaVuSansMono-BoldOblique.ttf")
160
161    def deja_vu_sans: Family =
162      Family(
163        plain = "DejaVuSans.ttf",
164        bold = "DejaVuSans-Bold.ttf",
165        italic = "DejaVuSans-Oblique.ttf",
166        bold_italic = "DejaVuSans-BoldOblique.ttf")
167
168    def deja_vu_serif: Family =
169      Family(
170        plain = "DejaVuSerif.ttf",
171        bold = "DejaVuSerif-Bold.ttf",
172        italic = "DejaVuSerif-Italic.ttf",
173        bold_italic = "DejaVuSerif-BoldItalic.ttf")
174
175    def vacuous: Family = Family(plain = "Vacuous.sfd")
176  }
177
178
179  /* hinting */
180
181  // see https://www.freetype.org/ttfautohint/doc/ttfautohint.html
182  private def auto_hint(source: Path, target: Path)
183  {
184    Isabelle_System.bash("ttfautohint -i " +
185      File.bash_path(source) + " " + File.bash_path(target)).check
186  }
187
188  private def hinted_path(hinted: Boolean): Path =
189    if (hinted) Path.basic("ttf-hinted") else Path.basic("ttf")
190
191  private val hinting = List(false, true)
192
193
194  /* build fonts */
195
196  private def find_file(dirs: List[Path], name: String): Path =
197  {
198    val path = Path.explode(name)
199    dirs.collectFirst({ case dir if (dir + path).is_file => dir + path }) match {
200      case Some(file) => file
201      case None =>
202        error(cat_lines(
203          ("Failed to find font file " + path + " in directories:") ::
204            dirs.map(dir => "  " + dir.toString)))
205    }
206  }
207
208  val default_sources: List[Family] =
209    List(Family.deja_vu_sans_mono, Family.deja_vu_sans, Family.deja_vu_serif)
210
211  val default_target_dir: Path = Path.explode("isabelle_fonts")
212
213  def build_fonts(
214    sources: List[Family] = default_sources,
215    source_dirs: List[Path] = Nil,
216    target_prefix: String = "Isabelle",
217    target_version: String = "",
218    target_dir: Path = default_target_dir,
219    progress: Progress = No_Progress)
220  {
221    progress.echo("Directory " + target_dir)
222    hinting.foreach(hinted => Isabelle_System.mkdirs(target_dir + hinted_path(hinted)))
223
224    val font_dirs = source_dirs ::: List(Path.explode("~~/Admin/isabelle_fonts"))
225    for (dir <- font_dirs if !dir.is_dir) error("Bad source directory: " + dir)
226
227
228    // Isabelle fonts
229
230    val targets =
231      for { source <- sources; (source_font, index) <- source.fonts.zipWithIndex }
232      yield {
233        val isabelle_file = find_file(font_dirs, Family.isabelle_symbols.get(index))
234
235        val source_file = find_file(font_dirs, source_font)
236        val source_names = Fontforge.font_names(source_file)
237
238        val target_names = source_names.update(prefix = target_prefix, version = target_version)
239
240        Isabelle_System.with_tmp_file("font", "ttf")(tmp_file =>
241        {
242          for (hinted <- hinting) {
243            val target_file = target_dir + hinted_path(hinted) + target_names.ttf
244            progress.echo("Font " + target_file.toString + " ...")
245
246            if (hinted) auto_hint(source_file, tmp_file)
247            else File.copy(source_file, tmp_file)
248
249            Fontforge.execute(
250              Fontforge.commands(
251                Fontforge.open(isabelle_file),
252                Fontforge.select(Range.isabelle_font),
253                Fontforge.copy,
254                Fontforge.close,
255
256                Fontforge.open(tmp_file),
257                Fontforge.select(Range.base_font),
258                Fontforge.select_invert,
259                Fontforge.clear,
260                Fontforge.select(Range.isabelle_font),
261                Fontforge.paste,
262
263                target_names.set,
264                Fontforge.generate(target_file),
265                Fontforge.close)
266            ).check
267          }
268        })
269
270        (target_names.ttf, index)
271      }
272
273
274    // Vacuous font
275
276    {
277      val vacuous_file = find_file(font_dirs, Family.vacuous.get(0))
278
279      val target_names = Fontforge.font_names(vacuous_file)
280      val target_file = target_dir + hinted_path(false) + target_names.ttf
281
282      progress.echo("Font " + target_file.toString + " ...")
283
284      val domain =
285        (for ((name, index) <- targets if index == 0)
286          yield Fontforge.font_domain(target_dir + hinted_path(false) + name))
287        .flatten.toSet.toList.sorted
288
289      Fontforge.execute(
290        Fontforge.commands(
291          Fontforge.open(vacuous_file),
292          Fontforge.select(Range.vacuous_font),
293          Fontforge.copy) +
294
295        domain.map(code =>
296            Fontforge.commands(
297              Fontforge.select(Seq(code)),
298              Fontforge.paste))
299          .mkString("\n", "\n", "\n") +
300
301        Fontforge.commands(
302          Fontforge.generate(target_file),
303          Fontforge.close)
304      ).check
305    }
306
307
308    // etc/settings
309
310    val settings_path = Components.settings(target_dir)
311    Isabelle_System.mkdirs(settings_path.dir)
312
313    def fonts_settings(hinted: Boolean): String =
314      "\n  isabelle_fonts \\\n" +
315      (for ((target, _) <- targets) yield
316        """    "$COMPONENT/""" + hinted_path(hinted).file_name + "/" + target.file_name + "\"")
317      .mkString(" \\\n")
318
319    File.write(settings_path,
320      """# -*- shell-script -*- :mode=shellscript:
321
322if grep "isabelle_fonts_hinted.*=.*false" "$ISABELLE_HOME_USER/etc/preferences" >/dev/null 2>/dev/null
323then""" + fonts_settings(false) + """
324else""" + fonts_settings(true) + """
325fi
326
327isabelle_fonts_hidden "$COMPONENT/""" + hinted_path(false).file_name + """/Vacuous.ttf"
328""")
329
330
331    // README
332    File.copy(Path.explode("~~/Admin/isabelle_fonts/README"), target_dir)
333  }
334
335
336  /* Isabelle tool wrapper */
337
338  val isabelle_tool =
339    Isabelle_Tool("build_fonts", "construct Isabelle fonts", args =>
340    {
341      var source_dirs: List[Path] = Nil
342
343      val getopts = Getopts("""
344Usage: isabelle build_fonts [OPTIONS]
345
346  Options are:
347    -d DIR       additional source directory
348
349  Construct Isabelle fonts from DejaVu font families and Isabelle symbols.
350""",
351        "d:" -> (arg => source_dirs = source_dirs ::: List(Path.explode(arg))))
352
353      val more_args = getopts(args)
354      if (more_args.nonEmpty) getopts.usage()
355
356      val target_version = Date.Format("uuuuMMdd")(Date.now())
357      val target_dir = Path.explode("isabelle_fonts-" + target_version)
358
359      val progress = new Console_Progress
360
361      build_fonts(source_dirs = source_dirs, target_dir = target_dir,
362        target_version = target_version, progress = progress)
363    })
364}
365