[isabelle-dev] Scan and MORE

[Makarius]

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

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


 	Makarius