73 \indexdef{explode@ {\tt\slshape{}explode}}{in {\tt\slshape Symbol}} |
73 \indexdef{explode@ {\tt\slshape{}explode}}{in {\tt\slshape Symbol}} |
74 \index{explode@ {\tt\slshape{}explode}} |
74 \index{explode@ {\tt\slshape{}explode}} |
75 In the examples above we use the function @{ML Symbol.explode}, instead of the |
75 In the examples above we use the function @{ML Symbol.explode}, instead of the |
76 more standard library function @{ML explode}, for obtaining an input list for |
76 more standard library function @{ML explode}, for obtaining an input list for |
77 the parser. The reason is that @{ML Symbol.explode} is aware of character sequences, |
77 the parser. The reason is that @{ML Symbol.explode} is aware of character sequences, |
78 for example @{text "\\<foo>"}, that have a special meaning in Isabelle. To see |
78 for example @{text "\<foo>"}, that have a special meaning in Isabelle. To see |
79 the difference consider |
79 the difference consider |
80 |
80 |
81 @{ML_response_fake [display,gray] |
81 @{ML_response_fake [display,gray] |
82 "let |
82 "let |
83 val input = \"\\<foo> bar\" |
83 val input = \"\<foo> bar\" |
84 in |
84 in |
85 (explode input, Symbol.explode input) |
85 (explode input, Symbol.explode input) |
86 end" |
86 end" |
87 "([\"\\\", \"<\", \"f\", \"o\", \"o\", \">\", \" \", \"b\", \"a\", \"r\"], |
87 "([\"\\\", \"<\", \"f\", \"o\", \"o\", \">\", \" \", \"b\", \"a\", \"r\"], |
88 [\"\\<foo>\", \" \", \"b\", \"a\", \"r\"])"} |
88 [\"\<foo>\", \" \", \"b\", \"a\", \"r\"])"} |
89 |
89 |
90 Slightly more general than the parser @{ML "$$"} is the function |
90 Slightly more general than the parser @{ML "$$"} is the function |
91 @{ML [index] one in Scan}, in that it takes a predicate as argument and |
91 @{ML [index] one in Scan}, in that it takes a predicate as argument and |
92 then parses exactly |
92 then parses exactly |
93 one item from the input list satisfying this predicate. For example the |
93 one item from the input list satisfying this predicate. For example the |