[isabelle-dev] Scan and MORE

[Stefan Berghofer]

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?

Hi Tim,

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

and

  val r2 = Scan.finite symbol.stopper (Scan.repeat scanner2) toks2

it should work as expected.

Greetings,
Stefan

-- 
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