ProgTutorial/Parsing.thy
changeset 221 a9eb69749c93
parent 220 fbcb89d84ba6
child 222 1dc03eaa7cb9
child 226 98f53ab3722e
equal deleted inserted replaced
220:fbcb89d84ba6 221:a9eb69749c93
   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}\\