reject invalid codepoints. Basis.iscodepoint. fix german char in js

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