diff -r cd6e187c7c45 -r a904fcbbbdbc src/Pure/GUI/gui.scala --- a/src/Pure/GUI/gui.scala Thu Dec 26 15:38:21 2024 +0100 +++ b/src/Pure/GUI/gui.scala Thu Dec 26 15:38:57 2024 +0100 @@ -75,12 +75,14 @@ def make_bold(str: String): String = str def enclose_text(str: String): String = enclose(make_text(str)) def enclose_bold(str: String): String = enclose(make_bold(str)) + def spaces(n: Int): String = Symbol.spaces(n) } class Style_HTML extends Style { override def enclose(body: String): String = "" + body + "" override def make_text(str: String): String = HTML.output(str) override def make_bold(str: String): String = "" + make_text(str) + "" + override def spaces(n: Int): String = HTML.spaces(n) } abstract class Style_Symbol extends Style {