diff -r 98ecc0ed6af1 -r e711873dcb53 src/Pure/GUI/gui.scala --- a/src/Pure/GUI/gui.scala Thu Dec 26 16:16:28 2024 +0100 +++ b/src/Pure/GUI/gui.scala Thu Dec 26 16:33:46 2024 +0100 @@ -95,7 +95,11 @@ object Style_Plain extends Style { override def toString: String = "plain" } - object Style_HTML extends Style_HTML { override def toString: String = "html" } + object Style_HTML extends Style_HTML { + override def toString: String = "html" + def bullet: String = "\u2218" + def bullet_triangle: String = "\u25b9" + } object Style_Symbol_Encoded extends Style_Symbol { override def toString: String = "symbol_encoded"