[isabelle-dev] Parse.term

[Walther Neuper]

Hi,

following Stefan Berghofers presentation at the Isabelle Developer 
Workshop I find Parse.term behaving not as expected:

text {* should not Parse.term repeat until a non-term token is reached ? *}

ML {*

parse Parse.term "xxx +++ 111 end";

(*val it =

    ("\^E\^Ftoken\^Exxx\^E\^F\^E",

     [Token (("+++", ({}, {})), (SymIdent, "+++"), Slot), Token (("111", ({}, {})), (Nat, "111"), Slot),

      Token (("end", ({}, {})), (Command, "end"), Slot)])

    : string * Token.T list*)

parse (Scan.repeat Parse.term) "xxx +++ 111 end";

(*val it =

    (["\^E\^Ftoken\^Exxx\^E\^F\^E", "\^E\^Ftoken\^E+++\^E\^F\^E", "\^E\^Ftoken\^E111\^E\^F\^E"],

     [Token (("end", ({}, {})), (Command, "end"), Slot)])

    : string list * Token.T list*)

*}

text {* Parse.term stops at "Keyword" of outer syntax ?!?

         Should not be parsed according to inner syntax ? *}

ML {*

parse Parse.term "xxx + 111 end";

(*val it =

    ("\^E\^Ftoken\^Exxx\^E\^F\^E",

     [Token (("+", ({}, {})), (Keyword, "+"), Slot), Token (("111", ({}, {})), (Nat, "111"), Slot),

      Token (("end", ({}, {})), (Command, "end"), Slot)])

    : string * Token.T list*)

parse Parse.term "xxx +++ (111) end";

(*val it =

    ("\^E\^Ftoken\^Exxx\^E\^F\^E",

     [Token (("+++", ({}, {})), (SymIdent, "+++"), Slot), Token (("(", ({}, {})), (Keyword, "("), Slot),

      Token (("111", ({}, {})), (Nat, "111"), Slot), Token ((")", ({}, {})), (Keyword, ")"), Slot),

      Token (("end", ({}, {})), (Command, "end"), Slot)])

    : string * Token.T list*)

*}


What am I doing wrong ?

With kind regards,
Walther

PS: In the attached file I searched for where the inner syntax could 
come into Parse.term --- so far without success.

-- 
------------------------------------------------------------------------
Walther Neuper                          Mailto: neuper at ist.tugraz.at
Institute for Software Technology          Tel: +43-(0)316/873-5728
University of Technology                   Fax: +43-(0)316/873-5706
Graz, Austria                             Home: www.ist.tugraz.at/neuper
------------------------------------------------------------------------


-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: Test_Parse_Term.thy
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20100811/55ca5fce/attachment.ksh>