--- a/src/Pure/General/sha1.ML Mon Oct 17 15:00:46 2016 +0200
+++ b/src/Pure/General/sha1.ML Mon Oct 17 15:46:51 2016 +0200
@@ -42,7 +42,7 @@
fun hex_digit (text, w: Word32.word) =
let
val d = Word32.toInt (w andb 0wxf);
- val dig = if d < 10 then chr (ord "0" + d) else chr (ord "a" + d - 10);
+ val dig = if d < 10 then chr (Char.ord #"0" + d) else chr (Char.ord #"a" + d - 10);
in (dig ^ text, w >> 0w4) end;
fun hex_word w = #1 (funpow 8 hex_digit ("", w));
@@ -145,7 +145,7 @@
(* digesting *)
-fun hex_digit i = if i < 10 then chr (ord "0" + i) else chr (ord "a" + i - 10);
+fun hex_digit i = if i < 10 then chr (Char.ord #"0" + i) else chr (Char.ord #"a" + i - 10);
fun hex_string arr i =
let val c = CInterface.fromCchar (CInterface.offset i CInterface.Cchar arr)
--- a/src/Pure/General/symbol.ML Mon Oct 17 15:00:46 2016 +0200
+++ b/src/Pure/General/symbol.ML Mon Oct 17 15:46:51 2016 +0200
@@ -121,7 +121,7 @@
val is_symbolic_char = member (op =) (raw_explode "!#$%&*+-/<=>?@^_|~");
fun is_printable s =
- if is_char s then ord space <= ord s andalso ord s <= ord "~"
+ if is_char s then 32 <= ord s andalso ord s <= Char.ord #"~"
else is_utf8 s orelse raw_symbolic s;
fun is_control s =
@@ -148,17 +148,17 @@
fun is_ascii_letter s =
is_char s andalso
- (ord "A" <= ord s andalso ord s <= ord "Z" orelse
- ord "a" <= ord s andalso ord s <= ord "z");
+ (Char.ord #"A" <= ord s andalso ord s <= Char.ord #"Z" orelse
+ Char.ord #"a" <= ord s andalso ord s <= Char.ord #"z");
fun is_ascii_digit s =
- is_char s andalso ord "0" <= ord s andalso ord s <= ord "9";
+ is_char s andalso Char.ord #"0" <= ord s andalso ord s <= Char.ord #"9";
fun is_ascii_hex s =
is_char s andalso
- (ord "0" <= ord s andalso ord s <= ord "9" orelse
- ord "A" <= ord s andalso ord s <= ord "F" orelse
- ord "a" <= ord s andalso ord s <= ord "f");
+ (Char.ord #"0" <= ord s andalso ord s <= Char.ord #"9" orelse
+ Char.ord #"A" <= ord s andalso ord s <= Char.ord #"F" orelse
+ Char.ord #"a" <= ord s andalso ord s <= Char.ord #"f");
fun is_ascii_quasi "_" = true
| is_ascii_quasi "'" = true
@@ -172,11 +172,11 @@
fun is_ascii_letdig s = is_ascii_letter s orelse is_ascii_digit s orelse is_ascii_quasi s;
-fun is_ascii_lower s = is_char s andalso (ord "a" <= ord s andalso ord s <= ord "z");
-fun is_ascii_upper s = is_char s andalso (ord "A" <= ord s andalso ord s <= ord "Z");
+fun is_ascii_lower s = is_char s andalso (Char.ord #"a" <= ord s andalso ord s <= Char.ord #"z");
+fun is_ascii_upper s = is_char s andalso (Char.ord #"A" <= ord s andalso ord s <= Char.ord #"Z");
-fun to_ascii_lower s = if is_ascii_upper s then chr (ord s + ord "a" - ord "A") else s;
-fun to_ascii_upper s = if is_ascii_lower s then chr (ord s + ord "A" - ord "a") else s;
+fun to_ascii_lower s = if is_ascii_upper s then chr (ord s + Char.ord #"a" - Char.ord #"A") else s;
+fun to_ascii_upper s = if is_ascii_lower s then chr (ord s + Char.ord #"A" - Char.ord #"a") else s;
fun is_ascii_identifier s =
size s > 0 andalso is_ascii_letter (String.substring (s, 0, 1)) andalso
@@ -444,7 +444,7 @@
fun bump [] = ["a"]
| bump ("z" :: ss) = "a" :: bump ss
| bump (s :: ss) =
- if is_char s andalso ord "a" <= ord s andalso ord s < ord "z"
+ if is_char s andalso Char.ord #"a" <= ord s andalso ord s < Char.ord #"z"
then chr (ord s + 1) :: ss
else "a" :: s :: ss;
--- a/src/Pure/ML/ml_lex.ML Mon Oct 17 15:00:46 2016 +0200
+++ b/src/Pure/ML/ml_lex.ML Mon Oct 17 15:46:51 2016 +0200
@@ -235,7 +235,8 @@
val scan_escape =
Scan.one (member (op =) (raw_explode "\"\\abtnvfr") o Symbol_Pos.symbol) >> single ||
- $$$ "^" @@@ (Scan.one (fn (s, _) => ord "@" <= ord s andalso ord s <= ord "_") >> single) ||
+ $$$ "^" @@@
+ (Scan.one (fn (s, _) => Char.ord #"@" <= ord s andalso ord s <= Char.ord #"_") >> single) ||
Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) --
Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) --
Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) >> (fn ((a, b), c) => [a, b, c]);
--- a/src/Pure/PIDE/yxml.ML Mon Oct 17 15:00:46 2016 +0200
+++ b/src/Pure/PIDE/yxml.ML Mon Oct 17 15:46:51 2016 +0200
@@ -49,12 +49,15 @@
(* markers *)
-val X = chr 5;
-val Y = chr 6;
+val X_char = Char.chr 5;
+val Y_char = Char.chr 6;
+
+val X = String.str X_char;
+val Y = String.str Y_char;
val XY = X ^ Y;
val XYX = XY ^ X;
-val detect = exists_string (fn s => s = X orelse s = Y);
+fun detect s = Char.contains s X_char orelse Char.contains s Y_char;
(* output *)
@@ -94,12 +97,10 @@
(* splitting *)
-fun is_char s c = ord s = Char.ord c;
-
val split_string =
Substring.full #>
- Substring.tokens (is_char X) #>
- map (Substring.fields (is_char Y) #> map Substring.string);
+ Substring.tokens (fn c => c = X_char) #>
+ map (Substring.fields (fn c => c = Y_char) #> map Substring.string);
(* structural errors *)
--- a/src/Pure/Syntax/lexicon.ML Mon Oct 17 15:00:46 2016 +0200
+++ b/src/Pure/Syntax/lexicon.ML Mon Oct 17 15:46:51 2016 +0200
@@ -295,7 +295,7 @@
val scan_vname =
let
fun nat n [] = n
- | nat n (c :: cs) = nat (n * 10 + (ord c - ord "0")) cs;
+ | nat n (c :: cs) = nat (n * 10 + (ord c - Char.ord #"0")) cs;
fun idxname cs ds = (implode (rev cs), nat 0 ds);
fun chop_idx [] ds = idxname [] ds
@@ -371,9 +371,9 @@
local
-val ten = ord "0" + 10;
-val a = ord "a";
-val A = ord "A";
+val ten = Char.ord #"0" + 10;
+val a = Char.ord #"a";
+val A = Char.ord #"A";
val _ = a > A orelse raise Fail "Bad ASCII";
fun remap_hex c =
--- a/src/Pure/library.ML Mon Oct 17 15:00:46 2016 +0200
+++ b/src/Pure/library.ML Mon Oct 17 15:46:51 2016 +0200
@@ -596,7 +596,7 @@
local
- val zero = ord "0";
+ val zero = Char.ord #"0";
val small_int = 10000: int;
val small_int_table = Vector.tabulate (small_int, Int.toString);
in
@@ -620,7 +620,7 @@
fun read_radix_int radix cs =
let
- val zero = ord "0";
+ val zero = Char.ord #"0";
val limit = zero + radix;
fun scan (num, []) = (num, [])
| scan (num, c :: cs) =