equal
deleted
inserted
replaced
11 signature THY_SCAN = |
11 signature THY_SCAN = |
12 sig |
12 sig |
13 datatype token_kind = |
13 datatype token_kind = |
14 Keyword | Ident | LongIdent | Var | TypeVar | Nat | String | Verbatim | Ignore | EOF |
14 Keyword | Ident | LongIdent | Var | TypeVar | Nat | String | Verbatim | Ignore | EOF |
15 val name_of_kind: token_kind -> string |
15 val name_of_kind: token_kind -> string |
16 val tokenize: Scan.lexicon -> string -> (token_kind * string * int) list |
16 val tokenize: Scan.lexicon -> string list -> (token_kind * string * int) list |
17 end; |
17 end; |
18 |
18 |
19 structure ThyScan: THY_SCAN = |
19 structure ThyScan: THY_SCAN = |
20 struct |
20 struct |
21 |
21 |
136 | tok_x' => tok_x'); |
136 | tok_x' => tok_x'); |
137 |
137 |
138 |
138 |
139 (* tokenize *) |
139 (* tokenize *) |
140 |
140 |
141 fun tokenize lex str = |
141 fun tokenize lex chs = |
142 let |
142 let |
143 val chs = explode str; (*sic!*) |
|
144 val scan_toks = Scan.repeat (scan_token lex); |
143 val scan_toks = Scan.repeat (scan_token lex); |
145 val ignore = fn (Ignore, _, _) => true | _ => false; |
144 val ignore = fn (Ignore, _, _) => true | _ => false; |
146 in |
145 in |
147 (case Scan.error (Scan.finite' Symbol.stopper scan_toks) (Some 1, chs) of |
146 (case Scan.error (Scan.finite' Symbol.stopper scan_toks) (Some 1, chs) of |
148 (toks, (n, [])) => filter_out ignore toks @ [token EOF n "end-of-file"] |
147 (toks, (n, [])) => filter_out ignore toks @ [token EOF n "end-of-file"] |