* 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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
