[isabelle-dev] Attributes and local theories

[Andreas Schropp]

Hi Isabelle people, esp. Makarius,

it has come to my attention that attributes are
called with a theory, a proof context and a local theory
in this succession.
Is this transforming the input lthy onion from inside out?

The implementation manual states that I have to treat
all of them uniformly. This means that the attribute
transformation on a lthy would not result in
an update of the target context but of the auxilliary
context instead. Is this correct and is the target
guaranteed to be transformed in the same way beforehand?

Also, does this mean we store the information resulting
from attributes 3 times, namely in theories, contexts and
local theories, potentially without any sharing?

If in the process of a local theory transformation I want
to store information to be looked up later, but not escaping
the scope of the target, where should I store it?
In the auxilliary context or the target context?


Cheers,
   Andy