changeset 28904 | 3ef9489eeef5 |
parent 28856 | 5e009a80fe6d |
child 29318 | 6337d1cb2ba0 |
28903:b3fc3a62247a | 28904:3ef9489eeef5 |
---|---|
385 (* token translations *) |
385 (* token translations *) |
386 |
386 |
387 fun tokentrans_mode m trs = map (fn (s, f) => (m, s, f)) trs; |
387 fun tokentrans_mode m trs = map (fn (s, f) => (m, s, f)) trs; |
388 |
388 |
389 val standard_token_classes = |
389 val standard_token_classes = |
390 ["class", "tfree", "tvar", "free", "bound", "var", "num", "xnum", "xstr"]; |
390 ["class", "tfree", "tvar", "free", "bound", "var", "num", "float", "xnum", "xstr"]; |
391 |
391 |
392 val standard_token_markers = map (fn s => "_" ^ s) standard_token_classes; |
392 val standard_token_markers = map (fn s => "_" ^ s) standard_token_classes; |
393 |
393 |
394 |
394 |
395 (* pure_ext *) |
395 (* pure_ext *) |