--- a/src/Pure/General/html.scala Thu Dec 26 15:38:21 2024 +0100
+++ b/src/Pure/General/html.scala Thu Dec 26 15:38:57 2024 +0100
@@ -12,6 +12,20 @@
object HTML {
+ /* spaces (non-breaking) */
+
+ val space = "\u00a0"
+
+ private val static_spaces = space * 100
+
+ def spaces(n: Int): String = {
+ require(n >= 0, "negative spaces")
+ if (n == 0) ""
+ else if (n < static_spaces.length) static_spaces.substring(0, n)
+ else space * n
+ }
+
+
/* attributes */
class Attribute(val name: String, value: String) {