| author | wenzelm |
| Wed, 07 May 2014 12:59:15 +0200 | |
| changeset 56895 | f058120aaad4 |
| parent 55618 | 995162143ef4 |
| permissions | -rw-r--r-- |
|
51614
22d1dd43f089
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents:
diff
changeset
|
1 |
/* Title: Pure/System/isabelle_font.scala |
|
22d1dd43f089
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
|
22d1dd43f089
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents:
diff
changeset
|
3 |
|
|
22d1dd43f089
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents:
diff
changeset
|
4 |
Isabelle font support. |
|
22d1dd43f089
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents:
diff
changeset
|
5 |
*/ |
|
22d1dd43f089
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents:
diff
changeset
|
6 |
|
|
22d1dd43f089
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents:
diff
changeset
|
7 |
package isabelle |
|
22d1dd43f089
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents:
diff
changeset
|
8 |
|
| 55618 | 9 |
|
|
51614
22d1dd43f089
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents:
diff
changeset
|
10 |
import java.awt.{GraphicsEnvironment, Font}
|
|
22d1dd43f089
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents:
diff
changeset
|
11 |
import java.io.{FileInputStream, BufferedInputStream}
|
|
22d1dd43f089
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents:
diff
changeset
|
12 |
import javafx.scene.text.{Font => JFX_Font}
|
|
22d1dd43f089
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents:
diff
changeset
|
13 |
|
|
22d1dd43f089
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents:
diff
changeset
|
14 |
|
|
22d1dd43f089
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents:
diff
changeset
|
15 |
object Isabelle_Font |
|
22d1dd43f089
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents:
diff
changeset
|
16 |
{
|
|
22d1dd43f089
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents:
diff
changeset
|
17 |
def apply(family: String = "IsabelleText", size: Int = 1, bold: Boolean = false): Font = |
|
22d1dd43f089
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents:
diff
changeset
|
18 |
new Font(family, if (bold) Font.BOLD else Font.PLAIN, size) |
|
22d1dd43f089
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents:
diff
changeset
|
19 |
|
|
22d1dd43f089
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents:
diff
changeset
|
20 |
def install_fonts() |
|
22d1dd43f089
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents:
diff
changeset
|
21 |
{
|
|
22d1dd43f089
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents:
diff
changeset
|
22 |
val ge = GraphicsEnvironment.getLocalGraphicsEnvironment() |
|
22d1dd43f089
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents:
diff
changeset
|
23 |
for (font <- Path.split(Isabelle_System.getenv_strict("ISABELLE_FONTS")))
|
|
22d1dd43f089
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents:
diff
changeset
|
24 |
ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, font.file)) |
|
22d1dd43f089
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents:
diff
changeset
|
25 |
} |
|
22d1dd43f089
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents:
diff
changeset
|
26 |
|
|
22d1dd43f089
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents:
diff
changeset
|
27 |
def install_fonts_jfx() |
|
22d1dd43f089
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents:
diff
changeset
|
28 |
{
|
|
22d1dd43f089
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents:
diff
changeset
|
29 |
for (font <- Path.split(Isabelle_System.getenv_strict("ISABELLE_FONTS"))) {
|
|
22d1dd43f089
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents:
diff
changeset
|
30 |
val stream = new BufferedInputStream(new FileInputStream(font.file)) |
|
22d1dd43f089
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents:
diff
changeset
|
31 |
try { JFX_Font.loadFont(stream, 1.0) }
|
|
22d1dd43f089
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents:
diff
changeset
|
32 |
finally { stream.close }
|
|
22d1dd43f089
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents:
diff
changeset
|
33 |
} |
|
22d1dd43f089
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents:
diff
changeset
|
34 |
} |
|
22d1dd43f089
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents:
diff
changeset
|
35 |
} |
|
22d1dd43f089
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents:
diff
changeset
|
36 |