[isabelle-dev] Scan and MORE

[Timothy Bourke]

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://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20091022/830e52c3/attachment.sig>