Post by Dmitriy Traytel
local_setup ‹fn lthy =>
I had expected the last one to be 7 as well. Is there a way to make the changes to configuration options persistent in this respect?
If you really mean persistent in the sense of local theory targets, the
declaration needs to be applied via Local_Theory.declaration -- this
corresponds to Isar commands like 'declare' or 'declaration'.
Nonetheless, there is a slightly odd detail above for updates of the
hypothetical context on the surface: Local_Theory.open_target ..
Local_Theory.close_target is more disruptive than it needs to be. This
can be explained from the historical situation of still not fully
consolidated Local_Theory.restore / Local_Theory.reset.
See also this NEWS entry for the coming release
* Local_Theory.restore has been renamed to Local_Theory.reset to
emphasize its disruptive impact on the cumulative context, notably the
scope of 'private' or 'qualified' names. Note that Local_Theory.reset is
only appropriate when targets are managed, e.g. starting from a global
theory and returning to it. Regular definitional packages should use
balanced blocks of Local_Theory.open_target versus
Local_Theory.close_target instead. Rare INCOMPATIBILITY.
I will try to get rid of this extra Local_Theory.reset in
I will also try harder to motivate other people to eliminate remaining
uses of Local_Theory.restore / Local_Theory.reset from their own tools.
Lets see if we can finally sort this out for the coming release.