diff -r 6afd01d5ddd6 -r 8a8814ab36f6 src/Tools/jEdit/jedit_main/isabelle_sidekick.scala --- a/src/Tools/jEdit/jedit_main/isabelle_sidekick.scala Fri Dec 27 15:59:08 2024 +0100 +++ b/src/Tools/jEdit/jedit_main/isabelle_sidekick.scala Fri Dec 27 16:14:16 2024 +0100 @@ -48,7 +48,7 @@ HTML.output(_name.substring(i + n)) case _ => HTML.output(_name) } - "" + s + "" + GUI.Style_HTML.enclose_style(css, s) } override def getLongString: String = _name override def getName: String = _name