equal
deleted
inserted
replaced
39 parts: The first part consists of a collection of generic parser combinators |
39 parts: The first part consists of a collection of generic parser combinators |
40 defined in the structure @{ML_struct Scan} in the file @{ML_file |
40 defined in the structure @{ML_struct Scan} in the file @{ML_file |
41 "Pure/General/scan.ML"}. The second part of the library consists of |
41 "Pure/General/scan.ML"}. The second part of the library consists of |
42 combinators for dealing with specific token types, which are defined in the |
42 combinators for dealing with specific token types, which are defined in the |
43 structure @{ML_struct OuterParse} in the file @{ML_file |
43 structure @{ML_struct OuterParse} in the file @{ML_file |
44 "Pure/Isar/outer_parse.ML"}. In addition specific parsers for packages are |
44 "Pure/Isar/parse.ML"}. In addition specific parsers for packages are |
45 defined in @{ML_file "Pure/Isar/spec_parse.ML"}. Parsers for method arguments |
45 defined in @{ML_file "Pure/Isar/parse_spec.ML"}. Parsers for method arguments |
46 are defined in @{ML_file "Pure/Isar/args.ML"}. |
46 are defined in @{ML_file "Pure/Isar/args.ML"}. |
47 \end{readmore} |
47 \end{readmore} |
48 |
48 |
49 *} |
49 *} |
50 |
50 |
478 parsers for the arguments of proof methods, use the type @{ML_type |
478 parsers for the arguments of proof methods, use the type @{ML_type |
479 OuterLex.token}. |
479 OuterLex.token}. |
480 |
480 |
481 \begin{readmore} |
481 \begin{readmore} |
482 The parser functions for the theory syntax are contained in the structure |
482 The parser functions for the theory syntax are contained in the structure |
483 @{ML_struct OuterParse} defined in the file @{ML_file "Pure/Isar/outer_parse.ML"}. |
483 @{ML_struct OuterParse} defined in the file @{ML_file "Pure/Isar/parse.ML"}. |
484 The definition for tokens is in the file @{ML_file "Pure/Isar/outer_lex.ML"}. |
484 The definition for tokens is in the file @{ML_file "Pure/Isar/outer_lex.ML"}. |
485 \end{readmore} |
485 \end{readmore} |
486 |
486 |
487 The structure @{ML_struct OuterLex} defines several kinds of tokens (for |
487 The structure @{ML_struct OuterLex} defines several kinds of tokens (for |
488 example @{ML_ind Ident in OuterLex} for identifiers, @{ML Keyword in |
488 example @{ML_ind Ident in OuterLex} for identifiers, @{ML Keyword in |
908 *} |
908 *} |
909 |
909 |
910 text_raw {* |
910 text_raw {* |
911 \begin{exercise} |
911 \begin{exercise} |
912 Have a look at how the parser @{ML SpecParse.where_alt_specs} is implemented |
912 Have a look at how the parser @{ML SpecParse.where_alt_specs} is implemented |
913 in file @{ML_file "Pure/Isar/spec_parse.ML"}. This parser corresponds |
913 in file @{ML_file "Pure/Isar/parse_spec.ML"}. This parser corresponds |
914 to the ``where-part'' of the introduction rules given above. Below |
914 to the ``where-part'' of the introduction rules given above. Below |
915 we paraphrase the code of @{ML_ind where_alt_specs in SpecParse} adapted to our |
915 we paraphrase the code of @{ML_ind where_alt_specs in SpecParse} adapted to our |
916 purposes. |
916 purposes. |
917 \begin{isabelle} |
917 \begin{isabelle} |
918 *} |
918 *} |