--- 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"