286 "([\"f\", \"o\", \"o\", \" \", \"b\", \"a\", \"r\", \" \", \"f\", \"o\", \"o\"], [])"}

   286 "([\"f\", \"o\", \"o\", \" \", \"b\", \"a\", \"r\", \" \", \"f\", \"o\", \"o\"], [])"}

   287 

   287 

   288   where the function @{ML [index] not_eof in Symbol} ensures that we do not read beyond the 

   288   where the function @{ML [index] not_eof in Symbol} ensures that we do not read beyond the 

   289   end of the input string (i.e.~stopper symbol).

   289   end of the input string (i.e.~stopper symbol).

   290 

   290 

   292   The function @{ML "Scan.unless p q" for p q} takes two parsers: if the first one can 

   291   The function @{ML "Scan.unless p q" for p q} takes two parsers: if the first one can 

   293   parse the input, then the whole parser fails; if not, then the second is tried. Therefore

   292   parse the input, then the whole parser fails; if not, then the second is tried. Therefore

   294   

   293   

   295   @{ML_response_fake_both [display,gray] "Scan.unless ($$ \"h\") ($$ \"w\") (Symbol.explode \"hello\")"

   294   @{ML_response_fake_both [display,gray] "Scan.unless ($$ \"h\") ($$ \"w\") (Symbol.explode \"hello\")"

   296                                "Exception FAIL raised"}

   295                                "Exception FAIL raised"}