diff jslib/urweb.js @ 597:d49d58a69877

Injected a non-special-case datatype
author Adam Chlipala <adamc@hcoop.net>
date Thu, 08 Jan 2009 10:30:14 -0500
parents 102e81d975e3
children 4c2c740c6931
line wrap: on
line diff
--- a/jslib/urweb.js	Thu Jan 08 10:15:45 2009 -0500
+++ b/jslib/urweb.js	Thu Jan 08 10:30:14 2009 -0500
@@ -41,6 +41,10 @@
   s.h = cons(function() { x.innerHTML = s.v }, s.h);
 }
 
+function eh(x) {
+  return x.split("&").join("&amp;").split("<").join("&lt;").split(">").join("&gt;");
+}
+
 function ts(x) { return x.toString() }
 function bs(b) { return (b ? "True" : "False") }