+htmlEscapeChar '<' = "<"
+htmlEscapeChar '>' = ">"
+htmlEscapeChar '&' = "&"
+htmlEscapeChar '\'' = "'"
+htmlEscapeChar '\"' = """
+htmlEscapeChar c = [c]
+
+pre x = "\n<div class=pre style='white-space:nowrap'>"++ (pre' x) ++ "\n</div>\n"