[isabelle-dev] NEWS: auxiliary contexts

[Makarius]

On Mon, 16 Apr 2012, Brian Huffman wrote:

> Finally we have a mechanism similar to "Section" in Coq, a more 
> lightweight alternative to locales.

This is what Larry Paulson and Florian Kammüller actually started in 
1998/1999 and eventually became the fully-featured locale + interpretation 
system of today.  The basic contexts are useful independently of that, 
especially since they can be nested within themselves and the other 
(non-nestable) targets.

The nesting is also where some small problems might still persist, since 
the Haftmann-Wenzel sandwich looks now like a Neapolitan wafer.


> I already replaced a one-off locale with this new local context 
> (changeset 4d49f3ffe97e)

In that change you also group several "(in c)" into a single "context v 
begin ... end".  This generally helps to improve scalability of locale 
applications, since context switching is realatively heavy.

At some point I would like to see Isabelle/jEdit in assisting to manage 
such context rearrangements.


 	Makarius