410 token parsers take into account the kind of tokens. The first example shows |
410 token parsers take into account the kind of tokens. The first example shows |
411 how to generate a token list out of a string using the function |
411 how to generate a token list out of a string using the function |
412 @{ML_ind scan in OuterSyntax}. It is given the argument |
412 @{ML_ind scan in OuterSyntax}. It is given the argument |
413 @{ML "Position.none"} since, |
413 @{ML "Position.none"} since, |
414 at the moment, we are not interested in generating precise error |
414 at the moment, we are not interested in generating precise error |
415 messages. The following code\footnote{Note that because of a possible bug in |
415 messages. The following code |
416 the PolyML runtime system, the result is printed as @{text [quotes] "?"}, |
|
417 instead of the tokens.} |
|
418 |
416 |
419 |
417 |
420 @{ML_response_fake [display,gray] "OuterSyntax.scan Position.none \"hello world\"" |
418 @{ML_response_fake [display,gray] "OuterSyntax.scan Position.none \"hello world\"" |
421 "[Token (\<dots>,(Ident, \"hello\"),\<dots>), |
419 "[Token (\<dots>,(Ident, \"hello\"),\<dots>), |
422 Token (\<dots>,(Space, \" \"),\<dots>), |
420 Token (\<dots>,(Space, \" \"),\<dots>), |