diff -r cd6e187c7c45 -r a904fcbbbdbc src/Pure/General/html.scala
--- 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) {