diff -r 68a9ada23bf8 -r 70d2f72098df src/Pure/GUI/gui.scala --- a/src/Pure/GUI/gui.scala Fri Dec 27 18:01:34 2024 +0100 +++ b/src/Pure/GUI/gui.scala Fri Dec 27 19:49:45 2024 +0100 @@ -102,8 +102,8 @@ } } - def bullet: String = "\u2218" - def bullet_triangle: String = "\u25b9" + def regular_bullet: String = "\u2022" + def triangular_bullet: String = "\u2023" } abstract class Style_Symbol extends Style {