* Authentic syntax for *all* term constants: provides simple and
robust correspondence between formal entities and concrete syntax.
Substantial INCOMPATIBILITY concerning low-level syntax translations
(translation rules and translation functions in ML). Some hints on
upgrading:
- Many existing uses of 'syntax' and 'translations' can be replaced
by more modern 'notation' and 'abbreviation', which are
independent of this issue.
- 'translations' require markup within the AST; the term syntax
provides the following special forms:
CONST c -- produces syntax version of constant c from context
XCONST c -- literally c, checked as constant from context
c -- literally c, if declared by 'syntax'
Plain identifiers are treated as AST variables -- occasionally the
system indicates accidental variables via the error "rhs contains
extra variables".
- 'parse_translation' etc. in ML may use the following
antiquotations:
@{const_syntax c} -- ML version of "CONST c" above
@{syntax_const c} -- literally c (checked wrt. 'syntax' declarations)
Note that old non-authentic syntax was based on unqualified base
names, so all of the above would coincide. Recall that 'print_syntax'
and ML_command "set Syntax.trace_ast" help to diagnose syntax
problems.
