1.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala Fri Nov 30 14:21:28 2018 +0100
1.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Fri Nov 30 14:46:00 2018 +0100
1.3 @@ -32,7 +32,7 @@
1.4
1.5 class Keyword_Asset(keyword: String, text: String, range: Text.Range) extends IAsset
1.6 {
1.7 - private val css = GUI.imitate_font_css((new JLabel).getFont)
1.8 + private val css = GUI.imitate_font_css(GUI.label_font())
1.9
1.10 protected var _name = text
1.11 protected var _start = int_to_pos(range.start)