[isabelle-dev] Scan and MORE
timbob at bigpond.com
Thu Oct 22 06:29:00 CEST 2009
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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Size: 187 bytes
Desc: not available
More information about the isabelle-dev