diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/js/urweb.js | 5 | ||||
| -rw-r--r-- | lib/ur/basis.urs | 1 |
2 files changed, 3 insertions, 3 deletions
diff --git a/lib/js/urweb.js b/lib/js/urweb.js index 00637172..2d39bc69 100644 --- a/lib/js/urweb.js +++ b/lib/js/urweb.js @@ -2122,9 +2122,7 @@ function isBlank(c) { } function isSpace(c) { var cp = ord(c); - if (cp == 10) - return true; - if (cp == 13) + if (cp >= 10 && cp <= 13) return true; if (cp == 133) return true; @@ -2790,6 +2788,7 @@ function isPrint(c) { function toLower(c) { var cp = ord(c); + if (cp == 304) return chr(105); else if (cp >= 7312 && cp <= 7354) diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs index c9d6556b..c893e65d 100644 --- a/lib/ur/basis.urs +++ b/lib/ur/basis.urs @@ -80,6 +80,7 @@ val ord : char -> int val chr : int -> char val iscodepoint : int -> bool +val issingle : char -> bool (** String operations *) |