| changeset 69358 | 71ef6e6da3dc |
| parent 65130 | 695930882487 |
| child 69377 | 81ae5893c556 |
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Wed Nov 28 11:43:06 2018 +0100 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Wed Nov 28 12:05:50 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, Font_Info.main_family()) + private val css = GUI.imitate_font_css((new JLabel).getFont) protected var _name = text protected var _start = int_to_pos(range.start)