388 Token (\<dots>,(Space, \" \"),\<dots>), |
388 Token (\<dots>,(Space, \" \"),\<dots>), |
389 Token (\<dots>,(Ident, \"world\"),\<dots>)]"} |
389 Token (\<dots>,(Ident, \"world\"),\<dots>)]"} |
390 |
390 |
391 produces three tokens where the first and the last are identifiers, since |
391 produces three tokens where the first and the last are identifiers, since |
392 @{text [quotes] "hello"} and @{text [quotes] "world"} do not match any |
392 @{text [quotes] "hello"} and @{text [quotes] "world"} do not match any |
393 other syntactic category.\footnote{Note that because of a possible a bug in |
393 other syntactic category.\footnote{Note that because of a possible bug in |
394 the PolyML runtime system the result is printed as @{text [quotes] "?"}, instead of |
394 the PolyML runtime system, the result is printed as @{text [quotes] "?"}, instead of |
395 the tokens.} The second indicates a space. |
395 the tokens.} The second indicates a space. |
396 |
396 |
397 Many parsing functions later on will require spaces, comments and the like |
397 Many parsing functions later on will require spaces, comments and the like |
398 to have already been filtered out. So from now on we are going to use the |
398 to have already been filtered out. So from now on we are going to use the |
399 functions @{ML filter} and @{ML OuterLex.is_proper} do this. For example: |
399 functions @{ML filter} and @{ML OuterLex.is_proper} to do this. For example: |
400 |
400 |
401 @{ML_response_fake [display,gray] |
401 @{ML_response_fake [display,gray] |
402 "let |
402 "let |
403 val input = OuterSyntax.scan Position.none \"hello world\" |
403 val input = OuterSyntax.scan Position.none \"hello world\" |
404 in |
404 in |
421 "filtered_input \"inductive | for\"" |
421 "filtered_input \"inductive | for\"" |
422 "[Token (\<dots>,(Command, \"inductive\"),\<dots>), |
422 "[Token (\<dots>,(Command, \"inductive\"),\<dots>), |
423 Token (\<dots>,(Keyword, \"|\"),\<dots>), |
423 Token (\<dots>,(Keyword, \"|\"),\<dots>), |
424 Token (\<dots>,(Keyword, \"for\"),\<dots>)]"} |
424 Token (\<dots>,(Keyword, \"for\"),\<dots>)]"} |
425 |
425 |
426 you obtain a list consisting of only a command and two keyword tokens. |
426 you obtain a list consisting of only one command and two keyword tokens. |
427 If you want to see which keywords and commands are currently known to Isabelle, type in |
427 If you want to see which keywords and commands are currently known to Isabelle, type in |
428 the following code (you might have to adjust the @{ML print_depth} in order to |
428 the following code (you might have to adjust the @{ML print_depth} in order to |
429 see the complete list): |
429 see the complete list): |
430 |
430 |
431 @{ML_response_fake [display,gray] |
431 @{ML_response_fake [display,gray] |
496 |
496 |
497 The function @{ML "OuterParse.!!!"} can be used to force termination of the |
497 The function @{ML "OuterParse.!!!"} can be used to force termination of the |
498 parser in case of a dead end, just like @{ML "Scan.!!"} (see previous section). |
498 parser in case of a dead end, just like @{ML "Scan.!!"} (see previous section). |
499 Except that the error message of @{ML "OuterParse.!!!"} is fixed to be |
499 Except that the error message of @{ML "OuterParse.!!!"} is fixed to be |
500 @{text [quotes] "Outer syntax error"} |
500 @{text [quotes] "Outer syntax error"} |
501 with a relatively precise description of the failure. For example: |
501 together with a relatively precise description of the failure. For example: |
502 |
502 |
503 @{ML_response_fake [display,gray] |
503 @{ML_response_fake [display,gray] |
504 "let |
504 "let |
505 val input = filtered_input \"in |\" |
505 val input = filtered_input \"in |\" |
506 val parse_bar_then_in = OuterParse.$$$ \"|\" -- OuterParse.$$$ \"in\" |
506 val parse_bar_then_in = OuterParse.$$$ \"|\" -- OuterParse.$$$ \"in\" |
518 \end{exercise} |
518 \end{exercise} |
519 |
519 |
520 (FIXME: or give parser for numbers) |
520 (FIXME: or give parser for numbers) |
521 |
521 |
522 Whenever there is a possibility that the processing of user input can fail, |
522 Whenever there is a possibility that the processing of user input can fail, |
523 it is a good idea to give as much information about where the error |
523 it is a good idea to give all available information about where the error |
524 occurred. For this Isabelle can attach positional information to tokens |
524 occurred. For this Isabelle can attach positional information to tokens |
525 and then thread this information up the processing chain. To see this, |
525 and then thread this information up the processing chain. To see this, |
526 modify the function @{ML filtered_input} described earlier to |
526 modify the function @{ML filtered_input} described earlier to |
527 *} |
527 *} |
528 |
528 |
1012 section {* Methods (TBD) *} |
1012 section {* Methods (TBD) *} |
1013 |
1013 |
1014 text {* |
1014 text {* |
1015 (FIXME: maybe move to after the tactic section) |
1015 (FIXME: maybe move to after the tactic section) |
1016 |
1016 |
1017 Methods are a central to Isabelle. They are the ones you use for example |
1017 Methods are central to Isabelle. They are the ones you use for example |
1018 in \isacommand{apply}. To print out all currently known methods you can use the |
1018 in \isacommand{apply}. To print out all currently known methods you can use the |
1019 Isabelle command: |
1019 Isabelle command: |
1020 |
1020 |
1021 \begin{isabelle} |
1021 \begin{isabelle} |
1022 \isacommand{print\_methods}\\ |
1022 \isacommand{print\_methods}\\ |