Thanks Stefan and Makarius, On Oct 21 at 14:24 +0200, Stefan Berghofer wrote: > note that the Scan library is mainly intended for parsing infinite token > streams (that's what the MORE exception is used for). If you want to use > the combinators defined in Scan for parsing finite streams, you have to > apply the wrapper function Scan.finite to your parser. This function > adds a "stopper symbol" (i.e. a symbol that must not occur in the stream > to be parsed) to the end of the stream and removes it again after the > parser has terminated. This "stopper symbol" avoids that a MORE exception > is raised. If you invoke your parsers using > [...]
Your explanations have crystallised the vague understandings I'd gained working from the source alone. So much clarity comes from knowing the intent behind a mechanism! Thanks too to Christian Urban who pointed me to Chapter 4 of The Isabelle Programming Tutorial. This topic is also described very clearly there. Tim. -------------- next part -------------- A non-text attachment was scrubbed... Name: not available Type: application/pgp-signature Size: 187 bytes Desc: not available URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20091022/830e52c3/attachment.pgp>
