clarified signature: fonts are not dependent on GUI;
authorwenzelm
Wed, 28 Nov 2018 16:27:21 +0100
changeset 69368 6f360600eabc
parent 69367 34b7550b66c7
child 69369 6ecc85955e04
clarified signature: fonts are not dependent on GUI;
src/Pure/GUI/gui.scala
src/Pure/System/isabelle_fonts.scala
src/Pure/Tools/main.scala
--- 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 */