| changeset 357 | 80b56d9b322f |
| parent 346 | 0fea8b7a14a1 |
| child 361 | 8ba963a3e039 |
| 356:43df2d59fb98 | 357:80b56d9b322f |
|---|---|
78 \end{itemize} |
78 \end{itemize} |
79 |
79 |
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} in 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}, 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_ind 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 |
146 end" |
146 end" |
147 "((\"h\", [\"e\", \"l\", \"l\", \"o\"]), (\"w\", [\"o\", \"r\", \"l\", \"d\"]))"} |
147 "((\"h\", [\"e\", \"l\", \"l\", \"o\"]), (\"w\", [\"o\", \"r\", \"l\", \"d\"]))"} |
148 |
148 |
149 The functions @{ML_ind "|--" in Scan} and @{ML_ind "--|" in Scan} work like the sequencing |
149 The functions @{ML_ind "|--" in Scan} and @{ML_ind "--|" in Scan} work like the sequencing |
150 function for parsers, except that they discard the item being parsed by the |
150 function for parsers, except that they discard the item being parsed by the |
151 first (respectively second) parser. For example: |
151 first (respectively second) parser. That means the item being dropped is the |
152 one that @{ML_ind "|--" in Scan} and @{ML_ind "--|" in Scan} ``point'' away. |
|
153 For example: |
|
152 |
154 |
153 @{ML_response [display,gray] |
155 @{ML_response [display,gray] |
154 "let |
156 "let |
155 val just_e = $$ \"h\" |-- $$ \"e\" |
157 val just_e = $$ \"h\" |-- $$ \"e\" |
156 val just_h = $$ \"h\" --| $$ \"e\" |
158 val just_h = $$ \"h\" --| $$ \"e\" |