--- a/src/Tools/WWW_Find/unicode_symbols.ML Sun Jun 19 21:53:04 2011 +0200
+++ b/src/Tools/WWW_Find/unicode_symbols.ML Sun Jun 19 22:52:49 2011 +0200
@@ -87,10 +87,17 @@
$$$ "#" |-- (Scan.many (not_contains "\n") @@@ ($$$ "\n"))
>> token Comment;
+fun is_sym s =
+ Symbol.not_eof s andalso
+ (case Symbol.decode s of
+ Symbol.Sym _ => true
+ | Symbol.Ctrl _ => true
+ | _ => false);
+
fun tokenize syms =
let
val scanner =
- Scan.one (Symbol.is_symbolic o Symbol_Pos.symbol) >> (token Symbol o single) ||
+ Scan.one (is_sym o Symbol_Pos.symbol) >> (token Symbol o single) ||
scan_comment ||
scan_space ||
scan_code ||