added HTML.encode (in Scala), similar to HTML.output in ML;

--- a/src/Pure/Thy/html.scala	Sun May 30 21:59:15 2010 +0200
+++ b/src/Pure/Thy/html.scala	Sun May 30 23:40:24 2010 +0200
@@ -11,6 +11,24 @@
 
 object HTML
 {
+  // encode text
+
+  def encode(text: String): String =
+  {
+    val s = new StringBuilder
+    for (c <- text.iterator) c match {
+      case '<' => s ++= "&lt;"
+      case '>' => s ++= "&gt;"
+      case '&' => s ++= "&amp;"
+      case '"' => s ++= "&quot;"
+      case '\'' => s ++= "&#39;"
+      case '\n' => s ++= "<br/>"
+      case _ => s += c
+    }
+    s.toString
+  }
+
+
   // common elements and attributes
 
   val BODY = "body"