11 { |
11 { |
12 /* relevant codepoint ranges */ |
12 /* relevant codepoint ranges */ |
13 |
13 |
14 object Range |
14 object Range |
15 { |
15 { |
16 def plain_text: Seq[Int] = |
16 def base_font: Seq[Int] = |
17 (0x0020 to 0x007e) ++ // ASCII |
17 (0x0020 to 0x007e) ++ // ASCII |
18 (0x00a0 to 0x024f) ++ // Latin Extended-A/B |
18 (0x00a0 to 0x024f) ++ // Latin Extended-A/B |
19 (0x0400 to 0x04ff) ++ // Cyrillic |
19 (0x0400 to 0x04ff) ++ // Cyrillic |
20 (0x0590 to 0x05ff) ++ // Hebrew (non-mono) |
|
21 (0x0600 to 0x06ff) ++ // Arabic |
20 (0x0600 to 0x06ff) ++ // Arabic |
22 Seq( |
21 Seq( |
23 0x2018, // single quote |
22 0x2018, // single quote |
24 0x2019, // single quote |
23 0x2019, // single quote |
25 0x201a, // single quote |
24 0x201a, // single quote |
113 |
113 |
114 sealed case class Family( |
114 sealed case class Family( |
115 plain: String = "", |
115 plain: String = "", |
116 bold: String = "", |
116 bold: String = "", |
117 italic: String = "", |
117 italic: String = "", |
118 bold_italic: String = "", |
118 bold_italic: String = "") |
119 fallback: Option[Family] = None) |
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 } |
120 |
128 |
121 object Family |
129 object Family |
122 { |
130 { |
|
131 def isabelle_text: Family = |
|
132 Family( |
|
133 plain = "IsabelleText.sfd", |
|
134 bold = "IsabelleTextBold.sfd") |
|
135 |
123 def deja_vu_sans_mono: Family = |
136 def deja_vu_sans_mono: Family = |
124 Family( |
137 Family( |
125 plain = "DejaVuSansMono.ttf", |
138 plain = "DejaVuSansMono.ttf", |
126 bold = "DejaVuSansMono-Bold.ttf", |
139 bold = "DejaVuSansMono-Bold.ttf", |
127 italic = "DejaVuSansMono-Oblique.ttf", |
140 italic = "DejaVuSansMono-Oblique.ttf", |
128 bold_italic = "DejaVuSansMono-BoldOblique.ttf", |
141 bold_italic = "DejaVuSansMono-BoldOblique.ttf") |
129 fallback = Some(deja_vu_sans)) |
|
130 |
142 |
131 def deja_vu_sans: Family = |
143 def deja_vu_sans: Family = |
132 Family( |
144 Family( |
133 plain = "DejaVuSans.ttf", |
145 plain = "DejaVuSans.ttf", |
134 bold = "DejaVuSans-Bold.ttf", |
146 bold = "DejaVuSans-Bold.ttf", |
140 plain = "DejaVuSerif.ttf", |
152 plain = "DejaVuSerif.ttf", |
141 bold = "DejaVuSerif-Bold.ttf", |
153 bold = "DejaVuSerif-Bold.ttf", |
142 italic = "DejaVuSerif-Italic.ttf", |
154 italic = "DejaVuSerif-Italic.ttf", |
143 bold_italic = "DejaVuSerif-BoldItalic.ttf") |
155 bold_italic = "DejaVuSerif-BoldItalic.ttf") |
144 } |
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 } |
145 } |
236 } |