[isabelle-dev] Scan and MORE

[Timothy Bourke]

In the Scan structure, I don't understand why option and || don't
treat MORE exceptions as they do Fail exceptions.

For instance, after these three lines:
  val toks1 = ["I", "s", "I", "s", "a", "I", "s"];
  val scanner1 = ($$ "I" -- $$ "s" -- Scan.option ($$ "a"))
  val r1 = Scan.bulk scanner1 toks1

r1 is
 ([(("I", "s"), NONE), (("I", "s"), SOME "a")], ["I", "s"]),
whereas I would have preferred it to be:
 ([(("I", "s"), NONE), (("I", "s"), SOME "a"), (("I", "s"), NONE)], [])

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?

Or, should Scan.option and Scan.|| be altered, or Scan.permissive
exposed?

Thank you,

Tim.

-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 187 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20091021/fe274b89/attachment.sig>