# HG changeset patch # User wenzelm # Date 1735223937 -3600 # Node ID a904fcbbbdbc41e5443fca5cc15d95a33ce9ffd8 # Parent cd6e187c7c452aec0ade7669954db5b0ce313dab clarified signature; diff -r cd6e187c7c45 -r a904fcbbbdbc src/Pure/Admin/component_llncs.scala --- 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 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 { 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) {