Notations: reworking the treatment of only-parsing and only-printing notations.

The (old) original model for notations was to associated both a
parsing and a printing rule to a notation.

Progressively, it become more and more common to have only parsing
notations or even multiple expressions printed with the same notation.

The new model is to attach to a given scope, string and entry at most
one either only-parsing or mixed-parsing-printing rules + an
arbitrarily many unrelated only-printing rules.

Additionally, we anticipate the ability to selectively
activate/deactivate each of those.

This allows to fix in particular #9682 but also to have
more-to-the-point warnings in case a notation overrides or partially
overrides another one.

Rules for importing are not changed (see forthcoming #12984 though).

We also improve the output of "Print Scopes" so that it adds when a
notation is only-parsing, only-printing, or deactivated, or a
combination of those.

Fixes #4738
Fixes #9682
Fixes part 2 of #12908
Fixes #13112

0 files changed, 0 insertions, 0 deletions