[isabelle-dev] Auxiliary contexts again

[Makarius]

On Mon, 15 Oct 2012, Christian Sternagel wrote:

> Just out of curiosity. Why is it not allowed to "open" a named context 
> inside an auxiliary context?

The question is merely what is feasible to implement.  The challenge 
increases approximately along the following line of further development:

   (0) Non-nested targets and properly localized packages -- more or less 
established in the past few years, although some packages are still 
lacking localization, and we are still chewing some fine-points concerning 
targets.

   (1) Nested auxiliary contexts inside some outermost target: This is 
where we are getting half-way now.  The idea is rather old, but early this 
year I dared to open this can again.

   (2) Properly nested sub-target structure for bundles -- a reletively new 
thing, but not fully implemented yet.

   (3) Nesting of named targets inside any of the other context blocks 
above -- still far ahead and presently out of reach.


 	Makarius