author | wenzelm |
Thu, 22 Apr 2021 22:07:05 +0200 | |
changeset 73599 | 981df2e1f646 |
parent 73340 | 0ffcad1f6130 |
child 75393 | 87ebf5a50283 |
permissions | -rw-r--r-- |
69355 | 1 |
/* Title: Pure/System/isabelle_system.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Fonts from the Isabelle system environment, notably the "Isabelle DejaVu" |
|
5 |
collection. |
|
6 |
*/ |
|
7 |
||
8 |
package isabelle |
|
9 |
||
10 |
||
69368
6f360600eabc
clarified signature: fonts are not dependent on GUI;
wenzelm
parents:
69364
diff
changeset
|
11 |
import java.awt.{Font, GraphicsEnvironment} |
69360 | 12 |
|
13 |
||
69355 | 14 |
object Isabelle_Fonts |
15 |
{ |
|
69357 | 16 |
/* standard names */ |
17 |
||
18 |
val mono: String = "Isabelle DejaVu Sans Mono" |
|
19 |
val sans: String = "Isabelle DejaVu Sans" |
|
20 |
val serif: String = "Isabelle DejaVu Serif" |
|
21 |
||
22 |
||
69360 | 23 |
/* environment entries */ |
69355 | 24 |
|
69363 | 25 |
object Entry |
26 |
{ |
|
27 |
object Ordering extends scala.math.Ordering[Entry] |
|
28 |
{ |
|
29 |
def compare(entry1: Entry, entry2: Entry): Int = |
|
30 |
entry1.family compare entry2.family match { |
|
31 |
case 0 => entry1.style compare entry2.style |
|
32 |
case ord => ord |
|
33 |
} |
|
34 |
} |
|
35 |
} |
|
36 |
||
69374 | 37 |
sealed case class Entry(path: Path, hidden: Boolean = false) |
69360 | 38 |
{ |
69364
91dbade9a5fa
proper font file name for HTTP (amending dc9a39c3f75d);
wenzelm
parents:
69363
diff
changeset
|
39 |
lazy val bytes: Bytes = Bytes.read(path) |
91dbade9a5fa
proper font file name for HTTP (amending dc9a39c3f75d);
wenzelm
parents:
69363
diff
changeset
|
40 |
lazy val font: Font = Font.createFont(Font.TRUETYPE_FONT, path.file) |
69360 | 41 |
|
42 |
def family: String = font.getFamily |
|
43 |
def name: String = font.getFontName |
|
69363 | 44 |
def style: Int = |
45 |
(if (is_bold) Font.BOLD else 0) + |
|
46 |
(if (is_italic) Font.ITALIC else 0) |
|
69355 | 47 |
|
69363 | 48 |
// educated guess for style: Font.createFont always produces Font.PLAIN |
69360 | 49 |
private lazy val name_lowercase = Word.lowercase(name) |
50 |
def is_bold: Boolean = |
|
51 |
name_lowercase.containsSlice("bold") |
|
52 |
def is_italic: Boolean = |
|
69363 | 53 |
name_lowercase.containsSlice("italic") || |
54 |
name_lowercase.containsSlice("oblique") |
|
69360 | 55 |
} |
56 |
||
57 |
def make_entries( |
|
58 |
getenv: String => String = Isabelle_System.getenv_strict(_), |
|
69374 | 59 |
hidden: Boolean = false): List[Entry] = |
69355 | 60 |
{ |
69360 | 61 |
Path.split(getenv("ISABELLE_FONTS")).map(Entry(_)) ::: |
69374 | 62 |
(if (hidden) Path.split(getenv("ISABELLE_FONTS_HIDDEN")).map(Entry(_, hidden = true)) else Nil) |
69355 | 63 |
} |
69360 | 64 |
|
69363 | 65 |
private lazy val all_fonts: List[Entry] = |
69374 | 66 |
make_entries(hidden = true).sorted(Entry.Ordering) |
69360 | 67 |
|
69374 | 68 |
def fonts(hidden: Boolean = false): List[Entry] = |
69 |
if (hidden) all_fonts else all_fonts.filter(entry => !entry.hidden) |
|
69368
6f360600eabc
clarified signature: fonts are not dependent on GUI;
wenzelm
parents:
69364
diff
changeset
|
70 |
|
6f360600eabc
clarified signature: fonts are not dependent on GUI;
wenzelm
parents:
69364
diff
changeset
|
71 |
|
6f360600eabc
clarified signature: fonts are not dependent on GUI;
wenzelm
parents:
69364
diff
changeset
|
72 |
/* system init */ |
6f360600eabc
clarified signature: fonts are not dependent on GUI;
wenzelm
parents:
69364
diff
changeset
|
73 |
|
73340 | 74 |
def init(): Unit = |
69368
6f360600eabc
clarified signature: fonts are not dependent on GUI;
wenzelm
parents:
69364
diff
changeset
|
75 |
{ |
6f360600eabc
clarified signature: fonts are not dependent on GUI;
wenzelm
parents:
69364
diff
changeset
|
76 |
val ge = GraphicsEnvironment.getLocalGraphicsEnvironment() |
6f360600eabc
clarified signature: fonts are not dependent on GUI;
wenzelm
parents:
69364
diff
changeset
|
77 |
for (entry <- fonts()) ge.registerFont(entry.font) |
6f360600eabc
clarified signature: fonts are not dependent on GUI;
wenzelm
parents:
69364
diff
changeset
|
78 |
} |
69355 | 79 |
} |