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