[isabelle-dev] NEWS: outer syntax forward declarations

[Makarius]

* Prover IDE: support for user-defined Isar commands within the running 
session.

* Forward declaration of outer syntax keywords within the theory
header -- minor INCOMPATIBILITY for user-defined commands.  Allow new
commands to be used in the same theory where defined.

* Antiquotation @{keyword "name"} produces a parser for outer syntax
from a minor keyword introduced via theory header declaration.

* Antiquotation @{command_spec "name"} produces the
Outer_Syntax.command_spec from a major keyword introduced via theory
header declaration; it can be passed to Outer_Syntax.command etc.


This refers to Isabelle/95bd95addb24.

It is an important reform of an old issue, although the Isar command table 
is still not fully stateless.

Practically, it impacts maintenance of the main logic images, since they 
can now be edited freely with Isabelle/jEdit.  No need to fall back on 
Proof General / Emacs just for that ...


 	Makarius