1.1 --- a/src/Pure/Thy/html.scala	Sun May 30 21:59:15 2010 +0200
     1.2 +++ b/src/Pure/Thy/html.scala	Sun May 30 23:40:24 2010 +0200
     1.3 @@ -11,6 +11,24 @@
     1.4  
     1.5  object HTML
     1.6  {
     1.7 +  // encode text
     1.8 +
     1.9 +  def encode(text: String): String =
    1.10 +  {
    1.11 +    val s = new StringBuilder
    1.12 +    for (c <- text.iterator) c match {
    1.13 +      case '<' => s ++= "&lt;"
    1.14 +      case '>' => s ++= "&gt;"
    1.15 +      case '&' => s ++= "&amp;"
    1.16 +      case '"' => s ++= "&quot;"
    1.17 +      case '\'' => s ++= "&#39;"
    1.18 +      case '\n' => s ++= "<br/>"
    1.19 +      case _ => s += c
    1.20 +    }
    1.21 +    s.toString
    1.22 +  }
    1.23 +
    1.24 +
    1.25    // common elements and attributes
    1.26  
    1.27    val BODY = "body"