--- a/src/Pure/Admin/component_llncs.scala Thu Dec 26 15:38:21 2024 +0100
+++ b/src/Pure/Admin/component_llncs.scala Thu Dec 26 15:38:57 2024 +0100
@@ -59,7 +59,7 @@
/* README */
- File.change(component_dir.path + README_md)(_.replace(" ", "\u00a0"))
+ File.change(component_dir.path + README_md)(_.replace(" ", HTML.space))
File.write(component_dir.README,
"""This is the Springer LaTeX LNCS style for authors from
--- 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 = "<html>" + body + "</html>"
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)
}
abstract class Style_Symbol extends Style {
--- 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) {