69330
|
1 |
/* Title: Pure/Tools/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 |
{
|
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(
|
|
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
|
69331
|
30 |
0x204b, // FOOTNOTE
|
69330
|
31 |
0x20ac, // Euro
|
|
32 |
0xfb01, // ligature fi
|
|
33 |
0xfb02, // ligature fl
|
|
34 |
0xfffd, // replacement character
|
|
35 |
)
|
|
36 |
|
69336
|
37 |
def isabelle_font: Seq[Int] =
|
69330
|
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)
|
69336
|
51 |
(0x0590 to 0x05ff) ++ // Hebrew (non-mono)
|
69330
|
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(
|
69331
|
81 |
0x261b, // ACTION
|
69330
|
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(
|
69331
|
104 |
0x1f310, // globe with meridians (Symbola font)
|
|
105 |
0x1f4d3, // notebook (Symbola font)
|
|
106 |
0x1f5c0, // folder (Symbola font)
|
|
107 |
0x1f5cf, // page (Symbola font)
|
69330
|
108 |
)
|
|
109 |
}
|
|
110 |
|
|
111 |
|
|
112 |
/* font families */
|
|
113 |
|
69332
|
114 |
sealed case class Family(
|
|
115 |
plain: String = "",
|
|
116 |
bold: String = "",
|
|
117 |
italic: String = "",
|
69336
|
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 |
}
|
69330
|
128 |
|
|
129 |
object Family
|
|
130 |
{
|
69336
|
131 |
def isabelle_text: Family =
|
|
132 |
Family(
|
|
133 |
plain = "IsabelleText.sfd",
|
|
134 |
bold = "IsabelleTextBold.sfd")
|
|
135 |
|
69332
|
136 |
def deja_vu_sans_mono: Family =
|
69330
|
137 |
Family(
|
69332
|
138 |
plain = "DejaVuSansMono.ttf",
|
|
139 |
bold = "DejaVuSansMono-Bold.ttf",
|
|
140 |
italic = "DejaVuSansMono-Oblique.ttf",
|
69336
|
141 |
bold_italic = "DejaVuSansMono-BoldOblique.ttf")
|
69330
|
142 |
|
69332
|
143 |
def deja_vu_sans: Family =
|
69330
|
144 |
Family(
|
69332
|
145 |
plain = "DejaVuSans.ttf",
|
|
146 |
bold = "DejaVuSans-Bold.ttf",
|
|
147 |
italic = "DejaVuSans-Oblique.ttf",
|
|
148 |
bold_italic = "DejaVuSans-BoldOblique.ttf")
|
69330
|
149 |
|
69332
|
150 |
def deja_vu_serif: Family =
|
69330
|
151 |
Family(
|
69332
|
152 |
plain = "DejaVuSerif.ttf",
|
|
153 |
bold = "DejaVuSerif-Bold.ttf",
|
|
154 |
italic = "DejaVuSerif-Italic.ttf",
|
|
155 |
bold_italic = "DejaVuSerif-BoldItalic.ttf")
|
69330
|
156 |
}
|
69336
|
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 |
}
|
69330
|
236 |
}
|