# HG changeset patch
# User wenzelm
# Date 1476712011 -7200
# Node ID ac2abc987cf9e700f7c4cd03b3816cf83b4e798b
# Parent  c8990e5feac9ea91a05bfab981b380504d843344
accomodate Poly/ML repository version, which treats singleton strings as boxed;

diff -r c8990e5feac9 -r ac2abc987cf9 src/Pure/General/sha1.ML
--- 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)
diff -r c8990e5feac9 -r ac2abc987cf9 src/Pure/General/symbol.ML
--- 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;
 
diff -r c8990e5feac9 -r ac2abc987cf9 src/Pure/ML/ml_lex.ML
--- 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]);
diff -r c8990e5feac9 -r ac2abc987cf9 src/Pure/PIDE/yxml.ML
--- 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 *)
diff -r c8990e5feac9 -r ac2abc987cf9 src/Pure/Syntax/lexicon.ML
--- 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 =
diff -r c8990e5feac9 -r ac2abc987cf9 src/Pure/library.ML
--- 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) =