src/Pure/Thy/html.scala

--- a/src/Pure/Thy/html.scala	Fri May 01 15:33:43 2015 +0200
+++ b/src/Pure/Thy/html.scala	Sun May 03 00:01:10 2015 +0200
@@ -28,7 +28,7 @@
         case '"' => result ++= """
         case '\'' => result ++= "'"
         case '\n' => result ++= "<br/>"
-        case c => result += c
+        case _ => result += c
       }
     def encode_chars(s: String) = s.iterator.foreach(encode_char(_))