[polyml] Strange syntax in PolyML Code

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