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