comparison lib/js/urweb.js @ 821:395a5d450cc0

Chars and more string operations
author Adam Chlipala <adamc@hcoop.net>
date Tue, 26 May 2009 12:25:06 -0400
parents 4585f744574a
children be0988e46336
comparison
equal deleted inserted replaced
820:91f465ded07e 821:395a5d450cc0
348 return x.split("&").join("&amp;").split("<").join("&lt;").split(">").join("&gt;"); 348 return x.split("&").join("&amp;").split("<").join("&lt;").split(">").join("&gt;");
349 } 349 }
350 350
351 function ts(x) { return x.toString() } 351 function ts(x) { return x.toString() }
352 function bs(b) { return (b ? "True" : "False") } 352 function bs(b) { return (b ? "True" : "False") }
353
354 function sub(x, i) { return x[i]; }
355 function suf(x, i) { return x.substring(i); }
353 356
354 function pi(s) { 357 function pi(s) {
355 var r = parseInt(s); 358 var r = parseInt(s);
356 if (r.toString() == s) 359 if (r.toString() == s)
357 return r; 360 return r;