88 by the programmer (for example to handle them). |
88 by the programmer (for example to handle them). |
89 |
89 |
90 In the examples above we use the function @{ML_ind explode in Symbol} from the |
90 In the examples above we use the function @{ML_ind explode in Symbol} from the |
91 structure @{ML_struct Symbol}, instead of the more standard library function |
91 structure @{ML_struct Symbol}, instead of the more standard library function |
92 @{ML_ind explode in String}, for obtaining an input list for the parser. The reason is |
92 @{ML_ind explode in String}, for obtaining an input list for the parser. The reason is |
93 that @{ML explode} in @{ML_struct Symbol} is aware of character |
93 that @{ML explode in Symbol} is aware of character |
94 sequences, for example @{text "\<foo>"}, that have a special meaning in |
94 sequences, for example @{text "\<foo>"}, that have a special meaning in |
95 Isabelle. To see the difference consider |
95 Isabelle. To see the difference consider |
96 |
96 |
97 @{ML_response_fake [display,gray] |
97 @{ML_response_fake [display,gray] |
98 "let |
98 "let |
99 val input = \"\<foo> bar\" |
99 val input = \"\<foo> bar\" |
100 in |
100 in |
101 (explode input, Symbol.explode input) |
101 (String.explode input, Symbol.explode input) |
102 end" |
102 end" |
103 "([\"\\\", \"<\", \"f\", \"o\", \"o\", \">\", \" \", \"b\", \"a\", \"r\"], |
103 "([\"\\\", \"<\", \"f\", \"o\", \"o\", \">\", \" \", \"b\", \"a\", \"r\"], |
104 [\"\<foo>\", \" \", \"b\", \"a\", \"r\"])"} |
104 [\"\<foo>\", \" \", \"b\", \"a\", \"r\"])"} |
105 |
105 |
106 Slightly more general than the parser @{ML "$$"} is the function |
106 Slightly more general than the parser @{ML "$$"} is the function |