69 |
71 |
70 @{ML_response_fake [display,gray] |
72 @{ML_response_fake [display,gray] |
71 "($$ \"x\") (Symbol.explode \"world\")" |
73 "($$ \"x\") (Symbol.explode \"world\")" |
72 "Exception FAIL raised"} |
74 "Exception FAIL raised"} |
73 |
75 |
74 will raise the exception @{text "FAIL"}. There are three exceptions used in |
76 will raise the exception @{text "FAIL"}. The function @{ML_ind "$$" in Scan} will also |
75 the parsing combinators: |
77 fail if you try to consume more than a single character. |
|
78 |
|
79 There are three exceptions that are raised by the parsing combinators: |
76 |
80 |
77 \begin{itemize} |
81 \begin{itemize} |
78 \item @{text "FAIL"} is used to indicate that alternative routes of parsing |
82 \item @{text "FAIL"} is used to indicate that alternative routes of parsing |
79 might be explored. |
83 might be explored. |
80 \item @{text "MORE"} indicates that there is not enough input for the parser. For example |
84 \item @{text "MORE"} indicates that there is not enough input for the parser. For example |
221 aborts the whole process of parsing in case of a failure and prints an error |
225 aborts the whole process of parsing in case of a failure and prints an error |
222 message. For example if you invoke the parser |
226 message. For example if you invoke the parser |
223 |
227 |
224 |
228 |
225 @{ML [display,gray] "!! (fn _ => fn _ =>\"foo\") ($$ \"h\")"} |
229 @{ML [display,gray] "!! (fn _ => fn _ =>\"foo\") ($$ \"h\")"} |
226 *} |
230 |
227 text {* |
|
228 on @{text [quotes] "hello"}, the parsing succeeds |
231 on @{text [quotes] "hello"}, the parsing succeeds |
229 |
232 |
230 @{ML_response [display,gray] |
233 @{ML_response [display,gray] |
231 "(!! (fn _ => fn _ => \"foo\") ($$ \"h\")) (Symbol.explode \"hello\")" |
234 "(!! (fn _ => fn _ => \"foo\") ($$ \"h\")) (Symbol.explode \"hello\")" |
232 "(\"h\", [\"e\", \"l\", \"l\", \"o\"])"} |
235 "(\"h\", [\"e\", \"l\", \"l\", \"o\"])"} |
239 then the parsing aborts and the error message @{text "foo"} is printed. In order to |
242 then the parsing aborts and the error message @{text "foo"} is printed. In order to |
240 see the error message properly, you need to prefix the parser with the function |
243 see the error message properly, you need to prefix the parser with the function |
241 @{ML_ind error in Scan}. For example: |
244 @{ML_ind error in Scan}. For example: |
242 |
245 |
243 @{ML_response_fake [display,gray] |
246 @{ML_response_fake [display,gray] |
244 "Scan.error (!! (fn _ => fn _ => \"foo\") ($$ \"h\"))" |
247 "Scan.error (!! (fn _ => fn _ => \"foo\") ($$ \"h\")) (Symbol.explode \"world\")" |
245 "Exception Error \"foo\" raised"} |
248 "Exception Error \"foo\" raised"} |
246 |
249 |
247 This ``prefixing'' is usually done by wrappers such as @{ML_ind local_theory in Outer_Syntax} |
250 This kind of ``prefixing'' to see the correct error message is usually done by wrappers |
|
251 such as @{ML_ind local_theory in Outer_Syntax} |
248 (see Section~\ref{sec:newcommand} which explains this function in more detail). |
252 (see Section~\ref{sec:newcommand} which explains this function in more detail). |
249 |
253 |
250 Let us now return to our example of parsing @{ML "(p -- q) || r" for p q |
254 Let us now return to our example of parsing @{ML "(p -- q) || r" for p q |
251 r}. If you want to generate the correct error message for failure |
255 r}. If you want to generate the correct error message for failure |
252 of parsing @{text "p"}-followed-by-@{text "q"}, then you have to write: |
256 of parsing @{text "p"}-followed-by-@{text "q"}, then you have to write: |