added is_utf8_trailer;
authorwenzelm
Sat, 12 Apr 2008 17:00:47 +0200
changeset 26632 90c0b075c0d3
parent 26631 d6b6c74a8bcf
child 26633 ff317b19e24e
added is_utf8_trailer;
src/Pure/General/symbol.ML
--- 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 *)