[isabelle-dev] NEWS: Pure as default presentation context

[Makarius]

*** Document preparation ***

* Outside of the inner theory body, the default presentation context is
theory Pure. Thus elementary antiquotations may be used in markup
commands (e.g. 'chapter', 'section', 'text') and formal comments.


This refers to Isabelle/146757999c8d. It is a spin-off from various
reorganisations of document output and antiquotations.

There is still some potential for surprise, because @{typ}, @{term},
@{thm} etc. in the theory header will use theory Pure and not the user's
theory. But it is possible to use the increasingly popular @{cartouche}
antiquotation (with its fancy syntax as a standalone cartouche).

Moreover, at some point I would like to introduce @{def} and @{ref}
antiquotations (e.g. for 'chapter', 'section') that serve as uniform
document labels -- in the overall session context, not the theory
proper. This would replace unchecked \label and \ref in LaTeX and open
further possibilities for formal references in big mathematical libraries.


	Makarius