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