[isabelle-dev] Scan and MORE
makarius at sketis.net
Wed Oct 21 16:38:44 CEST 2009
On Wed, 21 Oct 2009, Timothy Bourke wrote:
> Similarly for
> val toks2 = ["I", "s", "I", "s", "a", "I", "s"];
> val scanner2 = ($$ "I" -- $$ "s" -- $$ "a") >> K "Isa"
> || ($$ "I" -- $$ "s") >> K "Is"
> val r2 = Scan.bulk scanner2 toks2
> where r2 is
> (["Is", "Isa"], ["I", "s"])
> rather than
> (["Is", "Isa", "Is"], )
> Am I using the library incorrectly?
More notes in addition to what Stefan has already said:
* Scan.bulk is a rather obscure internal mechanism involved in cascading
of input sources. Grepping over the existing sources will show you
that it is rarely used, and indeed should not show up in user
Scan.repeat is what you want here, analogous to the REPEAT tactical.
(Maybe I need to find an even more obscure name for Scan.bulk.)
* Scanner combinators only really work with the proper wrappers, such as
Scan.finite or Scan.read. Setting up your own "framework" with proper
stoppers etc. is a bit tricky.
Applying combinator expressions directly to input tends to expose
certain internals that might make you wonder if it really works
correctly. (One weakness of the framework is in its non-abstracted
types. This was done that way many years ago, because there are
actually several variants rolled into one.)
More information about the isabelle-dev