equal
deleted
inserted
replaced
85 fun not_contains xs c = not (member (op =) (raw_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 is_sym s = |
|
91 Symbol.not_eof s andalso |
|
92 (case Symbol.decode s of |
|
93 Symbol.Sym _ => true |
|
94 | Symbol.Ctrl _ => true |
|
95 | _ => false); |
|
96 |
90 fun tokenize syms = |
97 fun tokenize syms = |
91 let |
98 let |
92 val scanner = |
99 val scanner = |
93 Scan.one (Symbol.is_symbolic o Symbol_Pos.symbol) >> (token Symbol o single) || |
100 Scan.one (is_sym o Symbol_Pos.symbol) >> (token Symbol o single) || |
94 scan_comment || |
101 scan_comment || |
95 scan_space || |
102 scan_space || |
96 scan_code || |
103 scan_code || |
97 Scan.literal keywords >> token Keyword || |
104 Scan.literal keywords >> token Keyword || |
98 scan_ascii_symbol || |
105 scan_ascii_symbol || |