72 (including quotes etc.). |
72 (including quotes etc.). |
73 |
73 |
74 * Inner syntax: identifiers in parse trees of generic categories |
74 * Inner syntax: identifiers in parse trees of generic categories |
75 "logic", "aprop", "idt" etc. carry position information (disguised as |
75 "logic", "aprop", "idt" etc. carry position information (disguised as |
76 type constraints). Occasional INCOMPATIBILITY with non-compliant |
76 type constraints). Occasional INCOMPATIBILITY with non-compliant |
77 translations that choke on unexpected type constraints: use |
77 translations that choke on unexpected type constraints. Positions can |
78 Syntax.strip_positions or Syntax.strip_positions_ast. As last resort, |
78 be stripped in ML translations via Syntax.strip_positions / |
79 reset the configuration option Syntax.positions, which is called |
79 Syntax.strip_positions_ast, or via the syntax constant |
80 "syntax_positions" in Isar attribute source. |
80 "_strip_positions" within parse trees. As last resort, positions can |
|
81 be disabled via the configuration option Syntax.positions, which is |
|
82 called "syntax_positions" in Isar attribute syntax. |
81 |
83 |
82 |
84 |
83 |
85 |
84 New in Isabelle2011 (January 2011) |
86 New in Isabelle2011 (January 2011) |
85 ---------------------------------- |
87 ---------------------------------- |