src/Tools/WWW_Find/unicode_symbols.ML

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