src/Tools/WWW_Find/unicode_symbols.ML
changeset 40527 e0c000e40c05
parent 36960 01594f816e3a
child 40627 becf5d5187cc
equal deleted inserted replaced
40526:ca3c6b1bfcdb 40527:e0c000e40c05
    64 fun is_eof (Token (EOF, _, _)) = true
    64 fun is_eof (Token (EOF, _, _)) = true
    65   | is_eof _ = false;
    65   | is_eof _ = false;
    66 
    66 
    67 fun end_position_of (Token (_, _, (_, epos))) = epos;
    67 fun end_position_of (Token (_, _, (_, epos))) = epos;
    68 
    68 
    69 val is_space = symbol #> (fn s => Symbol.is_blank s andalso s <> "\n");
    69 val is_space = Symbol_Pos.symbol #> (fn s => Symbol.is_blank s andalso s <> "\n");
    70 val scan_space =
    70 val scan_space =
    71   (Scan.many1 is_space @@@ Scan.optional ($$$ "\n") []
    71   (Scan.many1 is_space @@@ Scan.optional ($$$ "\n") []
    72    ||
    72    ||
    73    Scan.many is_space @@@ ($$$ "\n")) >> token Space;
    73    Scan.many is_space @@@ ($$$ "\n")) >> token Space;
    74 
    74 
    76 
    76 
    77 val scan_ascii_symbol = Scan.one
    77 val scan_ascii_symbol = Scan.one
    78   ((fn x => Symbol.is_ascii x andalso
    78   ((fn x => Symbol.is_ascii x andalso
    79       not (Symbol.is_ascii_letter x
    79       not (Symbol.is_ascii_letter x
    80            orelse Symbol.is_ascii_digit x
    80            orelse Symbol.is_ascii_digit x
    81            orelse Symbol.is_ascii_blank x)) o symbol)
    81            orelse Symbol.is_ascii_blank x)) o Symbol_Pos.symbol)
    82   -- Scan.many (not o Symbol.is_ascii_blank o 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 c));
    85 fun not_contains xs c = not (member (op =) (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 =
    91   let
    91   let
    92     val scanner =
    92     val scanner =
    93       Scan.one (Symbol.is_symbolic o symbol) >> (token Symbol o single) ||
    93       Scan.one (Symbol.is_symbolic o Symbol_Pos.symbol) >> (token Symbol o single) ||
    94       scan_comment ||
    94       scan_comment ||
    95       scan_space ||
    95       scan_space ||
    96       scan_code ||
    96       scan_code ||
    97       Scan.literal keywords >> token Keyword ||
    97       Scan.literal keywords >> token Keyword ||
    98       scan_ascii_symbol ||
    98       scan_ascii_symbol ||