--- a/src/Pure/GUI/gui.scala Wed Nov 28 16:18:40 2018 +0100
+++ b/src/Pure/GUI/gui.scala Wed Nov 28 16:27:21 2018 +0100
@@ -7,8 +7,7 @@
package isabelle
import java.lang.{ClassLoader, ClassNotFoundException, NoSuchMethodException}
-import java.awt.{GraphicsEnvironment, Image, Component, Container, Toolkit, Window, Font,
- KeyboardFocusManager}
+import java.awt.{Image, Component, Container, Toolkit, Window, Font, KeyboardFocusManager}
import java.awt.font.{TextAttribute, TransformAttribute, FontRenderContext, LineMetrics}
import java.awt.geom.AffineTransform
import javax.swing.{ImageIcon, JOptionPane, UIManager, JLayeredPane, JFrame, JWindow, JDialog,
@@ -242,11 +241,5 @@
def font(family: String = Isabelle_Fonts.sans, size: Int = 1, bold: Boolean = false): Font =
new Font(family, if (bold) Font.BOLD else Font.PLAIN, size)
-
- def install_fonts()
- {
- val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
- Isabelle_Fonts.fonts().foreach(entry => ge.registerFont(entry.font))
- }
}
--- a/src/Pure/System/isabelle_fonts.scala Wed Nov 28 16:18:40 2018 +0100
+++ b/src/Pure/System/isabelle_fonts.scala Wed Nov 28 16:27:21 2018 +0100
@@ -8,7 +8,7 @@
package isabelle
-import java.awt.Font
+import java.awt.{Font, GraphicsEnvironment}
object Isabelle_Fonts
@@ -67,4 +67,13 @@
def fonts(html: Boolean = false): List[Entry] =
if (html) all_fonts else all_fonts.filter(entry => !entry.html)
+
+
+ /* system init */
+
+ def init()
+ {
+ val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
+ for (entry <- fonts()) ge.registerFont(entry.font)
+ }
}
--- a/src/Pure/Tools/main.scala Wed Nov 28 16:18:40 2018 +0100
+++ b/src/Pure/Tools/main.scala Wed Nov 28 16:27:21 2018 +0100
@@ -20,7 +20,7 @@
{
try {
Isabelle_System.init()
- GUI.install_fonts()
+ Isabelle_Fonts.init()
/* ROOTS template */