equal
deleted
inserted
replaced
80 However, note that these exceptions are private to the parser and cannot be accessed |
80 However, note that these exceptions are private to the parser and cannot be accessed |
81 by the programmer (for example to handle them). |
81 by the programmer (for example to handle them). |
82 |
82 |
83 In the examples above we use the function @{ML_ind explode in Symbol} from the |
83 In the examples above we use the function @{ML_ind explode in Symbol} from the |
84 structure @{ML_struct Symbol}, instead of the more standard library function |
84 structure @{ML_struct Symbol}, instead of the more standard library function |
85 @{ML_ind explode}, for obtaining an input list for the parser. The reason is |
85 @{ML_ind explode in String}, for obtaining an input list for the parser. The reason is |
86 that @{ML_ind explode} in @{ML_struct Symbol} is aware of character |
86 that @{ML explode} in @{ML_struct Symbol} is aware of character |
87 sequences, for example @{text "\<foo>"}, that have a special meaning in |
87 sequences, for example @{text "\<foo>"}, that have a special meaning in |
88 Isabelle. To see the difference consider |
88 Isabelle. To see the difference consider |
89 |
89 |
90 @{ML_response_fake [display,gray] |
90 @{ML_response_fake [display,gray] |
91 "let |
91 "let |
778 text {* |
778 text {* |
779 Whenever types are given, they are stored in the @{ML SOME}s. The types are |
779 Whenever types are given, they are stored in the @{ML SOME}s. The types are |
780 not yet used to type the variables: this must be done by type-inference later |
780 not yet used to type the variables: this must be done by type-inference later |
781 on. Since types are part of the inner syntax they are strings with some |
781 on. Since types are part of the inner syntax they are strings with some |
782 encoded information (see previous section). If a mixfix-syntax is |
782 encoded information (see previous section). If a mixfix-syntax is |
783 present for a variable, then it is stored in the @{ML_ind Mixfix} data structure; |
783 present for a variable, then it is stored in the |
|
784 @{ML Mixfix}\footnote{FIXME: access to Mixfix data structure} data structure; |
784 no syntax translation is indicated by @{ML_ind NoSyn}. |
785 no syntax translation is indicated by @{ML_ind NoSyn}. |
785 |
786 |
786 \begin{readmore} |
787 \begin{readmore} |
787 The data structure for mixfix annotations is defined in @{ML_file "Pure/Syntax/mixfix.ML"}. |
788 The data structure for mixfix annotations is defined in @{ML_file "Pure/Syntax/mixfix.ML"}. |
788 \end{readmore} |
789 \end{readmore} |