--- 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 *)