diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/js/urweb.js | 7 | ||||
| -rw-r--r-- | lib/ur/basis.urs | 2 |
2 files changed, 8 insertions, 1 deletions
diff --git a/lib/js/urweb.js b/lib/js/urweb.js index de1a2ad0..c7725e28 100644 --- a/lib/js/urweb.js +++ b/lib/js/urweb.js @@ -38,7 +38,12 @@ function isXdigit(c) { return isDigit(c) || (c >= 'a' && c <= 'f') || (c >= 'A' function ord(c) { return c.charCodeAt(0); } function isPrint(c) { return ord(c) > 31 && ord(c) != 127; } function toLower(c) { return c.toLowerCase(); } -function toUpper(c) { return c.toUpperCase(); } +function toUpper(c) { + if (ord(c) == 223) + return c; + else + return c.toUpperCase(); +} // Lists diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs index 878f2793..c9d6556b 100644 --- a/lib/ur/basis.urs +++ b/lib/ur/basis.urs @@ -79,6 +79,8 @@ val toupper : char -> char val ord : char -> int val chr : int -> char +val iscodepoint : int -> bool + (** String operations *) val strlen : string -> int |