1 /* Title: Pure/Admin/isabelle_fonts.scala |
|
2 Author: Makarius |
|
3 |
|
4 Construction of Isabelle fonts. |
|
5 */ |
|
6 |
|
7 package isabelle |
|
8 |
|
9 |
|
10 object Isabelle_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 0x2018, // single quote |
|
23 0x2019, // single quote |
|
24 0x201a, // single quote |
|
25 0x201c, // double quote |
|
26 0x201d, // double quote |
|
27 0x201e, // double quote |
|
28 0x2039, // single guillemet |
|
29 0x203a, // single guillemet |
|
30 0x204b, // FOOTNOTE |
|
31 0x20ac, // Euro |
|
32 0xfb01, // ligature fi |
|
33 0xfb02, // ligature fl |
|
34 0xfffd, // replacement character |
|
35 ) |
|
36 |
|
37 def isabelle_font: Seq[Int] = |
|
38 Seq( |
|
39 0x05, // X |
|
40 0x06, // Y |
|
41 0x07, // EOF |
|
42 0x7f, // DEL |
|
43 0xac, // logicalnot |
|
44 0xb0, // degree |
|
45 0xb1, // plusminus |
|
46 0xb7, // periodcentered |
|
47 0xd7, // multiply |
|
48 0xf7, // divide |
|
49 ) ++ |
|
50 (0x0370 to 0x03ff) ++ // Greek (pseudo math) |
|
51 (0x0590 to 0x05ff) ++ // Hebrew (non-mono) |
|
52 Seq( |
|
53 0x2010, // hyphen |
|
54 0x2013, // dash |
|
55 0x2014, // dash |
|
56 0x2015, // dash |
|
57 0x2020, // dagger |
|
58 0x2021, // double dagger |
|
59 0x2022, // bullet |
|
60 0x2026, // ellipsis |
|
61 0x2030, // perthousand |
|
62 0x2032, // minute |
|
63 0x2033, // second |
|
64 0x2038, // caret |
|
65 0x20cd, // currency symbol |
|
66 ) ++ |
|
67 (0x2100 to 0x214f) ++ // Letterlike Symbols |
|
68 (0x2190 to 0x21ff) ++ // Arrows |
|
69 (0x2200 to 0x22ff) ++ // Mathematical Operators |
|
70 (0x2300 to 0x23ff) ++ // Miscellaneous Technical |
|
71 Seq( |
|
72 0x2423, // graphic for space |
|
73 0x2500, // box drawing |
|
74 0x2501, // box drawing |
|
75 0x2508, // box drawing |
|
76 0x2509, // box drawing |
|
77 0x2550, // box drawing |
|
78 ) ++ |
|
79 (0x25a0 to 0x25ff) ++ // Geometric Shapes |
|
80 Seq( |
|
81 0x261b, // ACTION |
|
82 0x2660, // spade suit |
|
83 0x2661, // heart suit |
|
84 0x2662, // diamond suit |
|
85 0x2663, // club suit |
|
86 0x266d, // musical flat |
|
87 0x266e, // musical natural |
|
88 0x266f, // musical sharp |
|
89 0x2756, // UNDEFINED |
|
90 0x2759, // BOLD |
|
91 0x27a7, // DESCR |
|
92 0x27e6, // left white square bracket |
|
93 0x27e7, // right white square bracket |
|
94 0x27e8, // left angle bracket |
|
95 0x27e9, // right angle bracket |
|
96 ) ++ |
|
97 (0x27f0 to 0x27ff) ++ // Supplemental Arrows-A |
|
98 (0x2900 to 0x297f) ++ // Supplemental Arrows-B |
|
99 (0x2980 to 0x29ff) ++ // Miscellaneous Mathematical Symbols-B |
|
100 (0x2a00 to 0x2aff) ++ // Supplemental Mathematical Operators |
|
101 Seq(0x2b1a) ++ // VERBATIM |
|
102 (0x1d400 to 0x1d7ff) ++ // Mathematical Alphanumeric Symbols |
|
103 Seq( |
|
104 0x1f310, // globe with meridians (Symbola font) |
|
105 0x1f4d3, // notebook (Symbola font) |
|
106 0x1f5c0, // folder (Symbola font) |
|
107 0x1f5cf, // page (Symbola font) |
|
108 ) |
|
109 } |
|
110 |
|
111 |
|
112 /* font families */ |
|
113 |
|
114 sealed case class Family( |
|
115 plain: String = "", |
|
116 bold: String = "", |
|
117 italic: String = "", |
|
118 bold_italic: String = "") |
|
119 { |
|
120 val fonts: List[String] = |
|
121 proper_string(plain).toList ::: |
|
122 proper_string(bold).toList ::: |
|
123 proper_string(italic).toList ::: |
|
124 proper_string(bold_italic).toList |
|
125 |
|
126 def get(index: Int): String = fonts(index % fonts.length) |
|
127 } |
|
128 |
|
129 object Family |
|
130 { |
|
131 def isabelle_text: Family = |
|
132 Family( |
|
133 plain = "IsabelleText.sfd", |
|
134 bold = "IsabelleTextBold.sfd") |
|
135 |
|
136 def deja_vu_sans_mono: Family = |
|
137 Family( |
|
138 plain = "DejaVuSansMono.ttf", |
|
139 bold = "DejaVuSansMono-Bold.ttf", |
|
140 italic = "DejaVuSansMono-Oblique.ttf", |
|
141 bold_italic = "DejaVuSansMono-BoldOblique.ttf") |
|
142 |
|
143 def deja_vu_sans: Family = |
|
144 Family( |
|
145 plain = "DejaVuSans.ttf", |
|
146 bold = "DejaVuSans-Bold.ttf", |
|
147 italic = "DejaVuSans-Oblique.ttf", |
|
148 bold_italic = "DejaVuSans-BoldOblique.ttf") |
|
149 |
|
150 def deja_vu_serif: Family = |
|
151 Family( |
|
152 plain = "DejaVuSerif.ttf", |
|
153 bold = "DejaVuSerif-Bold.ttf", |
|
154 italic = "DejaVuSerif-Italic.ttf", |
|
155 bold_italic = "DejaVuSerif-BoldItalic.ttf") |
|
156 } |
|
157 |
|
158 |
|
159 /* build fonts */ |
|
160 |
|
161 private def find_file(dirs: List[Path], name: String): Path = |
|
162 { |
|
163 val path = Path.explode(name) |
|
164 dirs.collectFirst({ case dir if (dir + path).is_file => dir + path }) match { |
|
165 case Some(file) => file |
|
166 case None => |
|
167 error(cat_lines( |
|
168 ("Failed to find font file " + path + " in directories:") :: |
|
169 dirs.map(dir => " " + dir.toString))) |
|
170 } |
|
171 } |
|
172 |
|
173 val default_sources: List[Family] = |
|
174 List(Family.deja_vu_sans_mono, Family.deja_vu_sans, Family.deja_vu_serif) |
|
175 |
|
176 def build_fonts( |
|
177 sources: List[Family] = default_sources, |
|
178 source_dirs: List[Path] = Nil, |
|
179 target_prefix: String = "Isabelle", |
|
180 target_version: String = "", |
|
181 target_dir: Path = Path.current, |
|
182 progress: Progress = No_Progress) |
|
183 { |
|
184 Isabelle_System.mkdirs(target_dir) |
|
185 |
|
186 val font_dirs = source_dirs ::: List(Path.explode("~~/lib/fonts")) |
|
187 |
|
188 for (isabelle_font <- Family.isabelle_text.fonts) { |
|
189 val isabelle_file = find_file(font_dirs, isabelle_font) |
|
190 val isabelle_names = Fontforge.font_names(isabelle_file) |
|
191 |
|
192 val target_names = isabelle_names.update(version = target_version) |
|
193 val target_file = target_dir + target_names.ttf |
|
194 |
|
195 progress.echo("Creating " + target_file.toString + " ...") |
|
196 Fontforge.execute( |
|
197 Fontforge.commands( |
|
198 Fontforge.open(isabelle_file), |
|
199 target_names.set, |
|
200 Fontforge.generate(target_file), |
|
201 Fontforge.close |
|
202 ) |
|
203 ).check |
|
204 } |
|
205 |
|
206 for { source <- sources; (source_font, index) <- source.fonts.zipWithIndex } { |
|
207 val isabelle_file = find_file(font_dirs, Family.isabelle_text.get(index)) |
|
208 |
|
209 val source_file = find_file(font_dirs, source_font) |
|
210 val source_names = Fontforge.font_names(source_file) |
|
211 |
|
212 val target_names = source_names.update(prefix = target_prefix, version = target_version) |
|
213 val target_file = target_dir + target_names.ttf |
|
214 |
|
215 progress.echo("Creating " + target_file.toString + " ...") |
|
216 Fontforge.execute( |
|
217 Fontforge.commands( |
|
218 Fontforge.open(isabelle_file), |
|
219 Fontforge.select(Range.isabelle_font), |
|
220 Fontforge.copy, |
|
221 Fontforge.close, |
|
222 |
|
223 Fontforge.open(source_file), |
|
224 Fontforge.select(Range.base_font), |
|
225 Fontforge.select_invert, |
|
226 Fontforge.clear, |
|
227 Fontforge.select(Range.isabelle_font), |
|
228 Fontforge.paste, |
|
229 |
|
230 target_names.set, |
|
231 Fontforge.generate(target_file), |
|
232 Fontforge.close) |
|
233 ).check |
|
234 } |
|
235 } |
|
236 |
|
237 |
|
238 /* Isabelle tool wrapper */ |
|
239 |
|
240 val isabelle_tool = |
|
241 Isabelle_Tool("build_fonts", "construct Isabelle fonts", args => |
|
242 { |
|
243 var source_dirs: List[Path] = Nil |
|
244 var target_dir = Path.current |
|
245 |
|
246 val getopts = Getopts(""" |
|
247 Usage: isabelle build_fonts [OPTIONS] |
|
248 |
|
249 Options are: |
|
250 -D DIR target directory (default ".") |
|
251 -d DIR additional source directory |
|
252 |
|
253 Construct Isabelle fonts from Deja Vu font families and Isabelle symbols. |
|
254 """, |
|
255 "D:" -> (arg => target_dir = Path.explode(arg)), |
|
256 "d:" -> (arg => source_dirs = source_dirs ::: List(Path.explode(arg)))) |
|
257 |
|
258 val more_args = getopts(args) |
|
259 if (more_args.nonEmpty) getopts.usage() |
|
260 |
|
261 val progress = new Console_Progress |
|
262 |
|
263 build_fonts(source_dirs = source_dirs, target_dir = target_dir, progress = progress) |
|
264 }) |
|
265 } |
|