src/Tools/jEdit/src/isabelle_sidekick.scala
changeset 69377 81ae5893c556
parent 69358 71ef6e6da3dc
     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)