# HG changeset patch
# User wenzelm
# Date 1208012447 -7200
# Node ID 90c0b075c0d3417ab20e6999dd0c6709890c814e
# Parent  d6b6c74a8bcf229f5cdb77c750c74cef7c0d374f
added is_utf8_trailer;

diff -r d6b6c74a8bcf -r 90c0b075c0d3 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 *)