353 "(((((\"h\", \"e\"), \"l\"), \"l\"), \"o\"), [\" \", \"w\", \"o\", \"r\", \"l\", \"d\"]) |
353 "(((((\"h\", \"e\"), \"l\"), \"l\"), \"o\"), [\" \", \"w\", \"o\", \"r\", \"l\", \"d\"]) |
354 : ((((string * string) * string) * string) * string) * string list"} |
354 : ((((string * string) * string) * string) * string) * string list"} |
355 Most of the time, however, we will have to deal with tokens that are not just strings. |
355 Most of the time, however, we will have to deal with tokens that are not just strings. |
356 The parsers for the theory syntax, as well as the parsers for the argument syntax |
356 The parsers for the theory syntax, as well as the parsers for the argument syntax |
357 of proof methods and attributes use the token type @{ML_type OuterParse.token}, |
357 of proof methods and attributes use the token type @{ML_type OuterParse.token}, |
358 which is identical to the type @{ML_type OuterLex.token}. |
358 which is identical to @{ML_type OuterLex.token}. |
359 The parser functions for the theory syntax are contained in the structure |
359 The parser functions for the theory syntax are contained in the structure |
360 @{ML_struct OuterParse} defined in the file @{ML_file "Pure/Isar/outer_parse.ML"}. |
360 @{ML_struct OuterParse} defined in the file @{ML_file "Pure/Isar/outer_parse.ML"}. |
361 In our parser, we will use the following functions: |
361 In our parser, we will use the following functions: |
362 \begin{mytable} |
362 \begin{mytable} |
363 @{ML_open "$$$ : string -> token list -> string * token list" (OuterParse)} \\ |
363 @{ML_open "$$$ : string -> token list -> string * token list" (OuterParse)} \\ |