# HG changeset patch
# User wenzelm
# Date 1543585560 -3600
# Node ID 81ae5893c556023e10c31e1546bd8b5c9229076e
# Parent  53194e2a969d9c2b44f554f01ee9d691bfe5ce71
use Isabelle fonts for all GUI look-and-feels;

diff -r 53194e2a969d -r 81ae5893c556 NEWS
--- a/NEWS	Fri Nov 30 14:21:28 2018 +0100
+++ b/NEWS	Fri Nov 30 14:46:00 2018 +0100
@@ -36,11 +36,10 @@
 
 * Fonts for the text area, gutter, GUI elements etc. use the "Isabelle
 DejaVu" collection by default, which provides uniform rendering quality
-with the usual Isabelle symbols. For Java/Swing GUI elements this
-requires the Metal look-and-feel: it is the default on Linux, but not
-macOS nor Windows. Line spacing no longer needs to be adjusted:
-properties for the old IsabelleText font had "Global Options / Text Area
-/ Extra vertical line spacing (in pixels): -2", now it defaults to 0.
+with the usual Isabelle symbols. Line spacing no longer needs to be
+adjusted: properties for the old IsabelleText font had "Global Options /
+Text Area / Extra vertical line spacing (in pixels): -2", now it
+defaults to 0.
 
 * Improved sub-pixel font rendering (especially on Linux), thanks to
 OpenJDK 11.
diff -r 53194e2a969d -r 81ae5893c556 src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Fri Nov 30 14:21:28 2018 +0100
+++ b/src/Pure/GUI/gui.scala	Fri Nov 30 14:46:00 2018 +0100
@@ -11,7 +11,7 @@
 import java.awt.font.{TextAttribute, TransformAttribute, FontRenderContext, LineMetrics}
 import java.awt.geom.AffineTransform
 import javax.swing.{ImageIcon, JOptionPane, UIManager, JLayeredPane, JFrame, JWindow, JDialog,
-  JButton, JTextField}
+  JButton, JTextField, JLabel}
 
 import scala.swing.{ComboBox, TextArea, ScrollPane}
 import scala.swing.event.SelectionChanged
@@ -224,6 +224,8 @@
   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 label_font(): Font = (new JLabel).getFont
+
 
   /* Isabelle fonts */
 
@@ -244,4 +246,15 @@
     val rel_size = line_metrics(font).getHeight.toDouble / line_metrics(font1).getHeight
     "font-family: " + family + "; font-size: " + (scale * rel_size * 100).toInt + "%;"
   }
+
+  def use_isabelle_fonts()
+  {
+    val default_font = label_font()
+    val ui = UIManager.getDefaults
+    for (prop <- List("Label.font", "TextArea.font", "TextPane.font", "Tooltip.font", "Tree.font"))
+    {
+      val font = ui.get(prop) match { case font: Font => font case _ => default_font }
+      ui.put(prop, GUI.imitate_font(font))
+    }
+  }
 }
diff -r 53194e2a969d -r 81ae5893c556 src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Fri Nov 30 14:21:28 2018 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Fri Nov 30 14:46:00 2018 +0100
@@ -32,7 +32,7 @@
 
   class Keyword_Asset(keyword: String, text: String, range: Text.Range) extends IAsset
   {
-    private val css = GUI.imitate_font_css((new JLabel).getFont)
+    private val css = GUI.imitate_font_css(GUI.label_font())
 
     protected var _name = text
     protected var _start = int_to_pos(range.start)
diff -r 53194e2a969d -r 81ae5893c556 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Fri Nov 30 14:21:28 2018 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Fri Nov 30 14:46:00 2018 +0100
@@ -399,6 +399,8 @@
             if (buffer != null && text_area != null) init_view(buffer, text_area)
           }
 
+          GUI.use_isabelle_fonts()
+
           spell_checker.update(options.value)
           session.update_options(options.value)