author | wenzelm |
Fri, 05 Apr 2019 23:45:35 +0200 | |
changeset 70071 | 9a03e9d5f336 |
parent 69885 | 6dc5506ad449 |
child 70072 | 54dc58086351 |
permissions | -rw-r--r-- |
69339 | 1 |
/* Title: Pure/Admin/build_fonts.scala |
69330 | 2 |
Author: Makarius |
3 |
||
69354 | 4 |
Build standard Isabelle fonts: DejaVu base + Isabelle symbols. |
69330 | 5 |
*/ |
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
69339 | 10 |
object Build_Fonts |
69330 | 11 |
{ |
12 |
/* relevant codepoint ranges */ |
|
13 |
||
14 |
object Range |
|
15 |
{ |
|
69336 | 16 |
def base_font: Seq[Int] = |
69330 | 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( |
|
69796 | 22 |
0x02dd, // hungarumlaut |
69330 | 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 |
|
69331 | 31 |
0x204b, // FOOTNOTE |
69330 | 32 |
0x20ac, // Euro |
69885 | 33 |
0x2710, // pencil |
69330 | 34 |
0xfb01, // ligature fi |
35 |
0xfb02, // ligature fl |
|
36 |
0xfffd, // replacement character |
|
37 |
) |
|
38 |
||
69336 | 39 |
def isabelle_font: Seq[Int] = |
69330 | 40 |
Seq( |
41 |
0x05, // X |
|
42 |
0x06, // Y |
|
43 |
0x07, // EOF |
|
44 |
0x7f, // DEL |
|
69341
6aa24ccd8049
proper superscript "-1", based on "Deja Vu Sans Condensed" U+207b/U+00b9, with bold version via "Change Weight / Embolden by 80 em units";
wenzelm
parents:
69339
diff
changeset
|
45 |
0xaf, // INVERSE |
69330 | 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) |
|
69336 | 54 |
(0x0590 to 0x05ff) ++ // Hebrew (non-mono) |
69330 | 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( |
|
69331 | 84 |
0x261b, // ACTION |
69330 | 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( |
|
69331 | 107 |
0x1f310, // globe with meridians (Symbola font) |
108 |
0x1f4d3, // notebook (Symbola font) |
|
109 |
0x1f5c0, // folder (Symbola font) |
|
110 |
0x1f5cf, // page (Symbola font) |
|
69330 | 111 |
) |
69371
3539767d5c61
generate Vacuous font from domain of Isabelle fonts;
wenzelm
parents:
69354
diff
changeset
|
112 |
|
69437
1b64f82aaf76
more mathematical glyphs from Isabelle2009-1/lib/fonts/IsabelleMono.sfd (still unused);
wenzelm
parents:
69436
diff
changeset
|
113 |
def isabelle_math_font: Seq[Int] = |
1b64f82aaf76
more mathematical glyphs from Isabelle2009-1/lib/fonts/IsabelleMono.sfd (still unused);
wenzelm
parents:
69436
diff
changeset
|
114 |
(0x21 to 0x2f) ++ // bang .. slash |
1b64f82aaf76
more mathematical glyphs from Isabelle2009-1/lib/fonts/IsabelleMono.sfd (still unused);
wenzelm
parents:
69436
diff
changeset
|
115 |
(0x3a to 0x40) ++ // colon .. atsign |
1b64f82aaf76
more mathematical glyphs from Isabelle2009-1/lib/fonts/IsabelleMono.sfd (still unused);
wenzelm
parents:
69436
diff
changeset
|
116 |
(0x5b to 0x5f) ++ // leftbracket .. underscore |
1b64f82aaf76
more mathematical glyphs from Isabelle2009-1/lib/fonts/IsabelleMono.sfd (still unused);
wenzelm
parents:
69436
diff
changeset
|
117 |
(0x7b to 0x7e) ++ // leftbrace .. tilde |
1b64f82aaf76
more mathematical glyphs from Isabelle2009-1/lib/fonts/IsabelleMono.sfd (still unused);
wenzelm
parents:
69436
diff
changeset
|
118 |
Seq( |
1b64f82aaf76
more mathematical glyphs from Isabelle2009-1/lib/fonts/IsabelleMono.sfd (still unused);
wenzelm
parents:
69436
diff
changeset
|
119 |
0xa9, // copyright |
1b64f82aaf76
more mathematical glyphs from Isabelle2009-1/lib/fonts/IsabelleMono.sfd (still unused);
wenzelm
parents:
69436
diff
changeset
|
120 |
0xae, // registered |
1b64f82aaf76
more mathematical glyphs from Isabelle2009-1/lib/fonts/IsabelleMono.sfd (still unused);
wenzelm
parents:
69436
diff
changeset
|
121 |
) |
1b64f82aaf76
more mathematical glyphs from Isabelle2009-1/lib/fonts/IsabelleMono.sfd (still unused);
wenzelm
parents:
69436
diff
changeset
|
122 |
|
1b64f82aaf76
more mathematical glyphs from Isabelle2009-1/lib/fonts/IsabelleMono.sfd (still unused);
wenzelm
parents:
69436
diff
changeset
|
123 |
val vacuous_font: Seq[Int] = |
1b64f82aaf76
more mathematical glyphs from Isabelle2009-1/lib/fonts/IsabelleMono.sfd (still unused);
wenzelm
parents:
69436
diff
changeset
|
124 |
Seq(0x3c) // "<" as template |
69330 | 125 |
} |
126 |
||
127 |
||
128 |
/* font families */ |
|
129 |
||
69332 | 130 |
sealed case class Family( |
131 |
plain: String = "", |
|
132 |
bold: String = "", |
|
133 |
italic: String = "", |
|
69336 | 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 |
} |
|
69330 | 144 |
|
145 |
object Family |
|
146 |
{ |
|
69436 | 147 |
def isabelle_symbols: Family = |
69336 | 148 |
Family( |
69436 | 149 |
plain = "IsabelleSymbols.sfd", |
150 |
bold = "IsabelleSymbolsBold.sfd") |
|
69336 | 151 |
|
69332 | 152 |
def deja_vu_sans_mono: Family = |
69330 | 153 |
Family( |
69332 | 154 |
plain = "DejaVuSansMono.ttf", |
155 |
bold = "DejaVuSansMono-Bold.ttf", |
|
156 |
italic = "DejaVuSansMono-Oblique.ttf", |
|
69336 | 157 |
bold_italic = "DejaVuSansMono-BoldOblique.ttf") |
69330 | 158 |
|
69332 | 159 |
def deja_vu_sans: Family = |
69330 | 160 |
Family( |
69332 | 161 |
plain = "DejaVuSans.ttf", |
162 |
bold = "DejaVuSans-Bold.ttf", |
|
163 |
italic = "DejaVuSans-Oblique.ttf", |
|
164 |
bold_italic = "DejaVuSans-BoldOblique.ttf") |
|
69330 | 165 |
|
69332 | 166 |
def deja_vu_serif: Family = |
69330 | 167 |
Family( |
69332 | 168 |
plain = "DejaVuSerif.ttf", |
169 |
bold = "DejaVuSerif-Bold.ttf", |
|
170 |
italic = "DejaVuSerif-Italic.ttf", |
|
171 |
bold_italic = "DejaVuSerif-BoldItalic.ttf") |
|
69371
3539767d5c61
generate Vacuous font from domain of Isabelle fonts;
wenzelm
parents:
69354
diff
changeset
|
172 |
|
3539767d5c61
generate Vacuous font from domain of Isabelle fonts;
wenzelm
parents:
69354
diff
changeset
|
173 |
def vacuous: Family = Family(plain = "Vacuous.sfd") |
69330 | 174 |
} |
69336 | 175 |
|
176 |
||
69795
4791988fcbc4
auto-hinting of original DejaVu fonts, but not Isabelle symbols;
wenzelm
parents:
69437
diff
changeset
|
177 |
/* auto-hinting */ |
4791988fcbc4
auto-hinting of original DejaVu fonts, but not Isabelle symbols;
wenzelm
parents:
69437
diff
changeset
|
178 |
// see https://www.freetype.org/ttfautohint/doc/ttfautohint.html |
4791988fcbc4
auto-hinting of original DejaVu fonts, but not Isabelle symbols;
wenzelm
parents:
69437
diff
changeset
|
179 |
|
4791988fcbc4
auto-hinting of original DejaVu fonts, but not Isabelle symbols;
wenzelm
parents:
69437
diff
changeset
|
180 |
def auto_hint(source: Path, target: Path) |
4791988fcbc4
auto-hinting of original DejaVu fonts, but not Isabelle symbols;
wenzelm
parents:
69437
diff
changeset
|
181 |
{ |
4791988fcbc4
auto-hinting of original DejaVu fonts, but not Isabelle symbols;
wenzelm
parents:
69437
diff
changeset
|
182 |
Isabelle_System.bash("ttfautohint -i " + |
4791988fcbc4
auto-hinting of original DejaVu fonts, but not Isabelle symbols;
wenzelm
parents:
69437
diff
changeset
|
183 |
File.bash_path(source) + " " + File.bash_path(target)).check |
4791988fcbc4
auto-hinting of original DejaVu fonts, but not Isabelle symbols;
wenzelm
parents:
69437
diff
changeset
|
184 |
} |
4791988fcbc4
auto-hinting of original DejaVu fonts, but not Isabelle symbols;
wenzelm
parents:
69437
diff
changeset
|
185 |
|
4791988fcbc4
auto-hinting of original DejaVu fonts, but not Isabelle symbols;
wenzelm
parents:
69437
diff
changeset
|
186 |
|
4791988fcbc4
auto-hinting of original DejaVu fonts, but not Isabelle symbols;
wenzelm
parents:
69437
diff
changeset
|
187 |
|
69336 | 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 |
||
69372 | 205 |
val default_target_dir: Path = Path.explode("isabelle_fonts") |
206 |
||
69336 | 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 = "", |
|
69372 | 212 |
target_dir: Path = default_target_dir, |
70071
9a03e9d5f336
option to bypass ttfautohint for experimentation (it can have adverse effects);
wenzelm
parents:
69885
diff
changeset
|
213 |
unhinted: Boolean = false, |
69336 | 214 |
progress: Progress = No_Progress) |
215 |
{ |
|
69372 | 216 |
progress.echo("Directory " + target_dir) |
69336 | 217 |
Isabelle_System.mkdirs(target_dir) |
218 |
||
69354 | 219 |
val font_dirs = source_dirs ::: List(Path.explode("~~/Admin/isabelle_fonts")) |
220 |
for (dir <- font_dirs if !dir.is_dir) error("Bad source directory: " + dir) |
|
69336 | 221 |
|
69371
3539767d5c61
generate Vacuous font from domain of Isabelle fonts;
wenzelm
parents:
69354
diff
changeset
|
222 |
|
3539767d5c61
generate Vacuous font from domain of Isabelle fonts;
wenzelm
parents:
69354
diff
changeset
|
223 |
// Isabelle fonts |
3539767d5c61
generate Vacuous font from domain of Isabelle fonts;
wenzelm
parents:
69354
diff
changeset
|
224 |
|
3539767d5c61
generate Vacuous font from domain of Isabelle fonts;
wenzelm
parents:
69354
diff
changeset
|
225 |
val targets = |
3539767d5c61
generate Vacuous font from domain of Isabelle fonts;
wenzelm
parents:
69354
diff
changeset
|
226 |
for { source <- sources; (source_font, index) <- source.fonts.zipWithIndex } |
3539767d5c61
generate Vacuous font from domain of Isabelle fonts;
wenzelm
parents:
69354
diff
changeset
|
227 |
yield { |
69436 | 228 |
val isabelle_file = find_file(font_dirs, Family.isabelle_symbols.get(index)) |
69371
3539767d5c61
generate Vacuous font from domain of Isabelle fonts;
wenzelm
parents:
69354
diff
changeset
|
229 |
|
3539767d5c61
generate Vacuous font from domain of Isabelle fonts;
wenzelm
parents:
69354
diff
changeset
|
230 |
val source_file = find_file(font_dirs, source_font) |
3539767d5c61
generate Vacuous font from domain of Isabelle fonts;
wenzelm
parents:
69354
diff
changeset
|
231 |
val source_names = Fontforge.font_names(source_file) |
3539767d5c61
generate Vacuous font from domain of Isabelle fonts;
wenzelm
parents:
69354
diff
changeset
|
232 |
|
3539767d5c61
generate Vacuous font from domain of Isabelle fonts;
wenzelm
parents:
69354
diff
changeset
|
233 |
val target_names = source_names.update(prefix = target_prefix, version = target_version) |
3539767d5c61
generate Vacuous font from domain of Isabelle fonts;
wenzelm
parents:
69354
diff
changeset
|
234 |
val target_file = target_dir + target_names.ttf |
3539767d5c61
generate Vacuous font from domain of Isabelle fonts;
wenzelm
parents:
69354
diff
changeset
|
235 |
|
69372 | 236 |
progress.echo("Font " + target_file.toString + " ...") |
69795
4791988fcbc4
auto-hinting of original DejaVu fonts, but not Isabelle symbols;
wenzelm
parents:
69437
diff
changeset
|
237 |
Isabelle_System.with_tmp_file("font", "ttf")(tmp_file => |
4791988fcbc4
auto-hinting of original DejaVu fonts, but not Isabelle symbols;
wenzelm
parents:
69437
diff
changeset
|
238 |
{ |
70071
9a03e9d5f336
option to bypass ttfautohint for experimentation (it can have adverse effects);
wenzelm
parents:
69885
diff
changeset
|
239 |
if (unhinted) File.copy(source_file, tmp_file) |
9a03e9d5f336
option to bypass ttfautohint for experimentation (it can have adverse effects);
wenzelm
parents:
69885
diff
changeset
|
240 |
else auto_hint(source_file, tmp_file) |
69795
4791988fcbc4
auto-hinting of original DejaVu fonts, but not Isabelle symbols;
wenzelm
parents:
69437
diff
changeset
|
241 |
|
4791988fcbc4
auto-hinting of original DejaVu fonts, but not Isabelle symbols;
wenzelm
parents:
69437
diff
changeset
|
242 |
Fontforge.execute( |
4791988fcbc4
auto-hinting of original DejaVu fonts, but not Isabelle symbols;
wenzelm
parents:
69437
diff
changeset
|
243 |
Fontforge.commands( |
4791988fcbc4
auto-hinting of original DejaVu fonts, but not Isabelle symbols;
wenzelm
parents:
69437
diff
changeset
|
244 |
Fontforge.open(isabelle_file), |
4791988fcbc4
auto-hinting of original DejaVu fonts, but not Isabelle symbols;
wenzelm
parents:
69437
diff
changeset
|
245 |
Fontforge.select(Range.isabelle_font), |
4791988fcbc4
auto-hinting of original DejaVu fonts, but not Isabelle symbols;
wenzelm
parents:
69437
diff
changeset
|
246 |
Fontforge.copy, |
4791988fcbc4
auto-hinting of original DejaVu fonts, but not Isabelle symbols;
wenzelm
parents:
69437
diff
changeset
|
247 |
Fontforge.close, |
69336 | 248 |
|
69795
4791988fcbc4
auto-hinting of original DejaVu fonts, but not Isabelle symbols;
wenzelm
parents:
69437
diff
changeset
|
249 |
Fontforge.open(tmp_file), |
4791988fcbc4
auto-hinting of original DejaVu fonts, but not Isabelle symbols;
wenzelm
parents:
69437
diff
changeset
|
250 |
Fontforge.select(Range.base_font), |
4791988fcbc4
auto-hinting of original DejaVu fonts, but not Isabelle symbols;
wenzelm
parents:
69437
diff
changeset
|
251 |
Fontforge.select_invert, |
4791988fcbc4
auto-hinting of original DejaVu fonts, but not Isabelle symbols;
wenzelm
parents:
69437
diff
changeset
|
252 |
Fontforge.clear, |
4791988fcbc4
auto-hinting of original DejaVu fonts, but not Isabelle symbols;
wenzelm
parents:
69437
diff
changeset
|
253 |
Fontforge.select(Range.isabelle_font), |
4791988fcbc4
auto-hinting of original DejaVu fonts, but not Isabelle symbols;
wenzelm
parents:
69437
diff
changeset
|
254 |
Fontforge.paste, |
69336 | 255 |
|
69795
4791988fcbc4
auto-hinting of original DejaVu fonts, but not Isabelle symbols;
wenzelm
parents:
69437
diff
changeset
|
256 |
target_names.set, |
4791988fcbc4
auto-hinting of original DejaVu fonts, but not Isabelle symbols;
wenzelm
parents:
69437
diff
changeset
|
257 |
Fontforge.generate(target_file), |
4791988fcbc4
auto-hinting of original DejaVu fonts, but not Isabelle symbols;
wenzelm
parents:
69437
diff
changeset
|
258 |
Fontforge.close) |
4791988fcbc4
auto-hinting of original DejaVu fonts, but not Isabelle symbols;
wenzelm
parents:
69437
diff
changeset
|
259 |
).check |
4791988fcbc4
auto-hinting of original DejaVu fonts, but not Isabelle symbols;
wenzelm
parents:
69437
diff
changeset
|
260 |
}) |
69371
3539767d5c61
generate Vacuous font from domain of Isabelle fonts;
wenzelm
parents:
69354
diff
changeset
|
261 |
|
3539767d5c61
generate Vacuous font from domain of Isabelle fonts;
wenzelm
parents:
69354
diff
changeset
|
262 |
(target_file, index) |
3539767d5c61
generate Vacuous font from domain of Isabelle fonts;
wenzelm
parents:
69354
diff
changeset
|
263 |
} |
3539767d5c61
generate Vacuous font from domain of Isabelle fonts;
wenzelm
parents:
69354
diff
changeset
|
264 |
|
3539767d5c61
generate Vacuous font from domain of Isabelle fonts;
wenzelm
parents:
69354
diff
changeset
|
265 |
|
3539767d5c61
generate Vacuous font from domain of Isabelle fonts;
wenzelm
parents:
69354
diff
changeset
|
266 |
// Vacuous font |
3539767d5c61
generate Vacuous font from domain of Isabelle fonts;
wenzelm
parents:
69354
diff
changeset
|
267 |
|
3539767d5c61
generate Vacuous font from domain of Isabelle fonts;
wenzelm
parents:
69354
diff
changeset
|
268 |
{ |
3539767d5c61
generate Vacuous font from domain of Isabelle fonts;
wenzelm
parents:
69354
diff
changeset
|
269 |
val vacuous_file = find_file(font_dirs, Family.vacuous.get(0)) |
3539767d5c61
generate Vacuous font from domain of Isabelle fonts;
wenzelm
parents:
69354
diff
changeset
|
270 |
|
3539767d5c61
generate Vacuous font from domain of Isabelle fonts;
wenzelm
parents:
69354
diff
changeset
|
271 |
val target_names = Fontforge.font_names(vacuous_file) |
69336 | 272 |
val target_file = target_dir + target_names.ttf |
273 |
||
69372 | 274 |
progress.echo("Font " + target_file.toString + " ...") |
69371
3539767d5c61
generate Vacuous font from domain of Isabelle fonts;
wenzelm
parents:
69354
diff
changeset
|
275 |
|
3539767d5c61
generate Vacuous font from domain of Isabelle fonts;
wenzelm
parents:
69354
diff
changeset
|
276 |
val domain = |
3539767d5c61
generate Vacuous font from domain of Isabelle fonts;
wenzelm
parents:
69354
diff
changeset
|
277 |
(for ((target_file, index) <- targets if index == 0) |
3539767d5c61
generate Vacuous font from domain of Isabelle fonts;
wenzelm
parents:
69354
diff
changeset
|
278 |
yield Fontforge.font_domain(target_file)).flatten.toSet.toList.sorted |
3539767d5c61
generate Vacuous font from domain of Isabelle fonts;
wenzelm
parents:
69354
diff
changeset
|
279 |
|
69336 | 280 |
Fontforge.execute( |
281 |
Fontforge.commands( |
|
69371
3539767d5c61
generate Vacuous font from domain of Isabelle fonts;
wenzelm
parents:
69354
diff
changeset
|
282 |
Fontforge.open(vacuous_file), |
3539767d5c61
generate Vacuous font from domain of Isabelle fonts;
wenzelm
parents:
69354
diff
changeset
|
283 |
Fontforge.select(Range.vacuous_font), |
3539767d5c61
generate Vacuous font from domain of Isabelle fonts;
wenzelm
parents:
69354
diff
changeset
|
284 |
Fontforge.copy) + |
69336 | 285 |
|
69371
3539767d5c61
generate Vacuous font from domain of Isabelle fonts;
wenzelm
parents:
69354
diff
changeset
|
286 |
domain.map(code => |
3539767d5c61
generate Vacuous font from domain of Isabelle fonts;
wenzelm
parents:
69354
diff
changeset
|
287 |
Fontforge.commands( |
3539767d5c61
generate Vacuous font from domain of Isabelle fonts;
wenzelm
parents:
69354
diff
changeset
|
288 |
Fontforge.select(Seq(code)), |
3539767d5c61
generate Vacuous font from domain of Isabelle fonts;
wenzelm
parents:
69354
diff
changeset
|
289 |
Fontforge.paste)) |
3539767d5c61
generate Vacuous font from domain of Isabelle fonts;
wenzelm
parents:
69354
diff
changeset
|
290 |
.mkString("\n", "\n", "\n") + |
69336 | 291 |
|
69371
3539767d5c61
generate Vacuous font from domain of Isabelle fonts;
wenzelm
parents:
69354
diff
changeset
|
292 |
Fontforge.commands( |
69336 | 293 |
Fontforge.generate(target_file), |
294 |
Fontforge.close) |
|
295 |
).check |
|
296 |
} |
|
69373 | 297 |
|
298 |
||
299 |
// etc/settings |
|
300 |
||
69395
d1c4a1dee9e7
more explicit support for Isabelle system components;
wenzelm
parents:
69374
diff
changeset
|
301 |
val settings_path = Components.settings(target_dir) |
69373 | 302 |
Isabelle_System.mkdirs(settings_path.dir) |
303 |
File.write(settings_path, |
|
304 |
"# -*- shell-script -*- :mode=shellscript:\n\nisabelle_fonts \\\n" + |
|
305 |
(for ((path, _) <- targets) |
|
306 |
yield """ "$COMPONENT/""" + path.file_name + "\"").mkString(" \\\n") + |
|
307 |
""" |
|
308 |
||
69374 | 309 |
isabelle_fonts_hidden "$COMPONENT/Vacuous.ttf" |
69373 | 310 |
""") |
311 |
||
312 |
||
313 |
// README |
|
314 |
File.copy(Path.explode("~~/Admin/isabelle_fonts/README"), target_dir) |
|
69336 | 315 |
} |
69337 | 316 |
|
317 |
||
318 |
/* Isabelle tool wrapper */ |
|
319 |
||
320 |
val isabelle_tool = |
|
321 |
Isabelle_Tool("build_fonts", "construct Isabelle fonts", args => |
|
322 |
{ |
|
323 |
var source_dirs: List[Path] = Nil |
|
70071
9a03e9d5f336
option to bypass ttfautohint for experimentation (it can have adverse effects);
wenzelm
parents:
69885
diff
changeset
|
324 |
var unhinted = false |
69337 | 325 |
|
326 |
val getopts = Getopts(""" |
|
327 |
Usage: isabelle build_fonts [OPTIONS] |
|
328 |
||
329 |
Options are: |
|
330 |
-d DIR additional source directory |
|
70071
9a03e9d5f336
option to bypass ttfautohint for experimentation (it can have adverse effects);
wenzelm
parents:
69885
diff
changeset
|
331 |
-u unhinted font (bypass ttfautohint) |
69337 | 332 |
|
69343
395c4fb15ea2
use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents:
69341
diff
changeset
|
333 |
Construct Isabelle fonts from DejaVu font families and Isabelle symbols. |
69337 | 334 |
""", |
70071
9a03e9d5f336
option to bypass ttfautohint for experimentation (it can have adverse effects);
wenzelm
parents:
69885
diff
changeset
|
335 |
"d:" -> (arg => source_dirs = source_dirs ::: List(Path.explode(arg))), |
9a03e9d5f336
option to bypass ttfautohint for experimentation (it can have adverse effects);
wenzelm
parents:
69885
diff
changeset
|
336 |
"u" -> (_ => unhinted = true)) |
69337 | 337 |
|
338 |
val more_args = getopts(args) |
|
339 |
if (more_args.nonEmpty) getopts.usage() |
|
340 |
||
69372 | 341 |
val target_version = Date.Format("uuuuMMdd")(Date.now()) |
342 |
val target_dir = Path.explode("isabelle_fonts-" + target_version) |
|
343 |
||
69337 | 344 |
val progress = new Console_Progress |
345 |
||
69372 | 346 |
build_fonts(source_dirs = source_dirs, target_dir = target_dir, |
70071
9a03e9d5f336
option to bypass ttfautohint for experimentation (it can have adverse effects);
wenzelm
parents:
69885
diff
changeset
|
347 |
target_version = target_version, unhinted = unhinted, progress = progress) |
69337 | 348 |
}) |
69330 | 349 |
} |