clarified signature;
authorwenzelm
Fri, 27 Dec 2024 15:59:08 +0100
changeset 81665 6afd01d5ddd6
parent 81664 201ec2e401cb
child 81666 8a8814ab36f6
clarified signature;
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"