--- 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.
--- 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))
+ }
+ }
}
--- 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)
--- 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)