src/Tools/WWW_Find/unicode_symbols.ML
changeset 40627 becf5d5187cc
parent 40527 e0c000e40c05
child 43469 882108e9536a
equal deleted inserted replaced
40626:d86540f6ea0d 40627:becf5d5187cc
    80            orelse Symbol.is_ascii_digit x
    80            orelse Symbol.is_ascii_digit x
    81            orelse Symbol.is_ascii_blank x)) o Symbol_Pos.symbol)
    81            orelse Symbol.is_ascii_blank x)) o Symbol_Pos.symbol)
    82   -- Scan.many (not o Symbol.is_ascii_blank o Symbol_Pos.symbol)
    82   -- Scan.many (not o Symbol.is_ascii_blank o Symbol_Pos.symbol)
    83   >> (token AsciiSymbol o op ::);
    83   >> (token AsciiSymbol o op ::);
    84 
    84 
    85 fun not_contains xs c = not (member (op =) (explode xs) (Symbol_Pos.symbol c));
    85 fun not_contains xs c = not (member (op =) (raw_explode xs) (Symbol_Pos.symbol c));
    86 val scan_comment =
    86 val scan_comment =
    87   $$$ "#" |-- (Scan.many (not_contains "\n") @@@ ($$$ "\n"))
    87   $$$ "#" |-- (Scan.many (not_contains "\n") @@@ ($$$ "\n"))
    88   >> token Comment;
    88   >> token Comment;
    89 
    89 
    90 fun tokenize syms =
    90 fun tokenize syms =