220   of @{text r}, not by the absence of @{text q} in the input. This kind of

   220   of @{text r}, not by the absence of @{text q} in the input. This kind of

   221   situation can be avoided when using the function @{ML "!!"}.  This function

   221   situation can be avoided when using the function @{ML "!!"}.  This function

   222   aborts the whole process of parsing in case of a failure and prints an error

   222   aborts the whole process of parsing in case of a failure and prints an error

   223   message. For example if you invoke the parser

   223   message. For example if you invoke the parser

   224 

   224 

   228   on @{text [quotes] "hello"}, the parsing succeeds

   229   on @{text [quotes] "hello"}, the parsing succeeds

   229 

   230 

   230   @{ML_response [display,gray] 

   231   @{ML_response [display,gray] 

   232   "(\"h\", [\"e\", \"l\", \"l\", \"o\"])"}

   233   "(\"h\", [\"e\", \"l\", \"l\", \"o\"])"}

   233 

   234 

   234   but if you invoke it on @{text [quotes] "world"}

   235   but if you invoke it on @{text [quotes] "world"}

   237                                "Exception ABORT raised"}

   238                                "Exception ABORT raised"}

   238 

   239 

   239   then the parsing aborts and the error message @{text "foo"} is printed. In order to

   240   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 

   241   see the error message properly, you need to prefix the parser with the function 

   241   @{ML_ind error in Scan}. For example:

   242   @{ML_ind error in Scan}. For example:

   242 

   243 

   243   @{ML_response_fake [display,gray] 

   244   @{ML_response_fake [display,gray] 

   245   "Exception Error \"foo\" raised"}

   246   "Exception Error \"foo\" raised"}

   246 

   247 

   247   This ``prefixing'' is usually done by wrappers such as @{ML_ind local_theory in Outer_Syntax} 

   248   This ``prefixing'' is usually done by wrappers such as @{ML_ind local_theory in Outer_Syntax} 

   248   (see Section~\ref{sec:newcommand} which explains this function in more detail). 

   249   (see Section~\ref{sec:newcommand} which explains this function in more detail). 

   249   

   250   

   254 

   255 

   255 ML{*fun p_followed_by_q p q r =

   256 ML{*fun p_followed_by_q p q r =

   256 let 

   257 let 

   257   val err_msg = fn _ => p ^ " is not followed by " ^ q

   258   val err_msg = fn _ => p ^ " is not followed by " ^ q

   258 in

   259 in

   260 end *}

   261 end *}

   261 

   262 

   262 

   263 

   263 text {*

   264 text {*

   264   Running this parser with the arguments

   265   Running this parser with the arguments