chars with more than 2 bytes are awkwardly handled by the "normal" string of javascript. the best way to get consistent results seems to be to convert to array by Array.from(...) and back to strings with .join("")

1 files changed, 7 insertions, 7 deletions

diff --git a/lib/js/urweb.js b/lib/js/urweb.js
index c7725e28..e28446e3 100644
--- a/lib/js/urweb.js
+++ b/lib/js/urweb.js
@@ -1462,9 +1462,9 @@ function s2b(s) { return s == "True" ? true : s == "False" ? false : null; }
 function s2be(s) { return s == "True" ? true : s == "False" ? false : er("Illegal Boolean " ^ s); }
 
 function id(x) { return x; }
-function sub(s, i) { return s.charAt(i); }
-function suf(s, i) { return s.substring(i); }
-function slen(s) { return s.length; }
+function sub(s, i) { return Array.from(s)[i].codePointAt(0); }
+function suf(s, i) { return Array.from(s).slice(i).join(""); }
+function slen(s) { return Array.from(s).length; }
 function sidx(s, ch) {
     var r = s.indexOf(ch);
     if (r == -1)
@@ -1494,10 +1494,10 @@ function schr(s, ch) {
         return s.substring(r);
 }
 function ssub(s, start, len) {
-    return s.substring(start, start+len);
+    return Array.from(s).slice(start, start+len).join("");
 }
 function strlenGe(s, len) {
-    return s.length >= len;
+    return slen(s) >= len;
 }
 
 function trimZeroes(s) {
@@ -1596,11 +1596,11 @@ function strcmp(str1, str2) {
 }
 
 function chr(n) {
-    return String.fromCharCode(n);
+    return String.fromCodePoint(n);
 }
 
 function htmlifySpecialChar(ch) {
-    return "&#" + ch.charCodeAt(0) + ";";
+    return "&#" + ch.codePointAt(0) + ";";
 }