--- a/src/Pure/General/symbol.ML Sat Apr 12 17:00:45 2008 +0200
+++ b/src/Pure/General/symbol.ML Sat Apr 12 17:00:47 2008 +0200
@@ -18,6 +18,7 @@
val is_char: symbol -> bool
val is_symbolic: symbol -> bool
val is_printable: symbol -> bool
+ val is_utf8_trailer: symbol -> bool
val eof: symbol
val is_eof: symbol -> bool
val stopper: symbol * (symbol -> bool)
@@ -111,6 +112,8 @@
if is_char s then ord space <= ord s andalso ord s <= ord "~"
else not (String.isPrefix "\\<^" s);
+fun is_utf8_trailer s = is_char s andalso 128 <= ord s andalso ord s < 192;
+
(* input source control *)