On Mon, 29 Jun 2009, Steven Obua wrote:
Hi, the "@" syntax is called an Anti-Quotation. PolyML knows nothing about
them. Isabelle preprocesses the ML files it read and replaces the
antiquotations before passing on the code to the PolyML compiler.
BTW, since people have asked this before: in Isabelle2009 the preprocesser
now coexists with regular ML token syntax. This means that antiquotations
within literal strings and comments are now longer expanded.
Moreover, since "@" can be part of a symbolic ML identifier, the "greatest
munch rule" of lexing might confuse people who don't like spaces. E.g. in
foo::@{thms bar}
the "::@" part is taken as a single ML name. Infixes are better
surrounded by spaces anyway, e.g.
foo :: @{thms bar}
(This discussion is better continued on the Isabelle mailing list.)
Makarius
_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
