# HG changeset patch
# User wenzelm
# Date 1308516769 -7200
# Node ID 882108e9536a6c0e906cf0d1916d7bbfcc599bc7
# Parent  265d9300d523cb5bccbf26bedb096244e97a06d0
accept control symbols;

diff -r 265d9300d523 -r 882108e9536a 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 ||