# 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)