src/Pure/GUI/gui.scala
changeset 81662 e711873dcb53
parent 81661 98ecc0ed6af1
child 81665 6afd01d5ddd6
--- 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"