# HG changeset patch
# User wenzelm
# Date 1735311548 -3600
# Node ID 6afd01d5ddd61590a0ad09bbfe99423e3e3e00e1
# Parent  201ec2e401cb107f2dd30143c1fcafaf2ac2aa6a
clarified signature;

diff -r 201ec2e401cb -r 6afd01d5ddd6 src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Fri Dec 27 14:31:38 2024 +0100
+++ b/src/Pure/GUI/gui.scala	Fri Dec 27 15:59:08 2024 +0100
@@ -83,6 +83,9 @@
     override def make_text(str: String): String = HTML.output(str)
     override def make_bold(str: String): String = "<b>" + make_text(str) + "</b>"
     override def spaces(n: Int): String = HTML.spaces(n)
+
+    def bullet: String = "\u2218"
+    def bullet_triangle: String = "\u25b9"
   }
 
   abstract class Style_Symbol extends Style {
@@ -95,11 +98,7 @@
 
   object Style_Plain extends Style { override def toString: String = "plain" }
 
-  object Style_HTML extends Style_HTML {
-    override def toString: String = "html"
-    def bullet: String = "\u2218"
-    def bullet_triangle: String = "\u25b9"
-  }
+  object Style_HTML extends Style_HTML { override def toString: String = "html" }
 
   object Style_Symbol_Encoded extends Style_Symbol {
     override def toString: String = "symbol_encoded"