changeset 81666 | 8a8814ab36f6 |
parent 81329 | 1775fdc7274e |
child 81671 | b18330f7bde0 |
--- 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) } - "<html><span style=\"" + css + "\">" + s + "</span></html>" + GUI.Style_HTML.enclose_style(css, s) } override def getLongString: String = _name override def getName: String = _name