[isabelle-dev] Scan and MORE
berghofe at in.tum.de
Wed Oct 21 14:24:15 CEST 2009
Timothy Bourke wrote:
> In the Scan structure, I don't understand why option and || don't
> treat MORE exceptions as they do Fail exceptions.
> Am I using the library incorrectly?
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
val r1 = Scan.finite Symbol.stopper (Scan.repeat scanner1) toks1
val r2 = Scan.finite symbol.stopper (Scan.repeat scanner2) toks2
it should work as expected.
Dr. Stefan Berghofer E-Mail: berghofe at in.tum.de
Institut fuer Informatik Phone: +49 89 289 17328
Technische Universitaet Muenchen Fax: +49 89 289 17307
Boltzmannstr. 3 Room: 01.11.059
85748 Garching, GERMANY http://www.in.tum.de/~berghofe
More information about the isabelle-dev