equal
deleted
inserted
replaced
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 = |
90 fun is_sym s = |
91 Symbol.not_eof s andalso |
91 (case Symbol.decode s of |
92 (case Symbol.decode s of |
92 Symbol.Sym _ => true |
93 Symbol.Sym _ => true |
93 | Symbol.Ctrl _ => true |
94 | Symbol.Ctrl _ => true |
94 | _ => false); |
95 | _ => false); |
|
96 |
95 |
97 fun tokenize syms = |
96 fun tokenize syms = |
98 let |
97 let |
99 val scanner = |
98 val scanner = |
100 Scan.one (is_sym o Symbol_Pos.symbol) >> (token Symbol o single) || |
99 Scan.one (is_sym o Symbol_Pos.symbol) >> (token Symbol o single) || |