Re: [isabelle] Behavior of configuration options in local theories



On 14/09/16 23:50, Makarius wrote:
		> See also this NEWS entry for the coming release
> (http://isabelle.in.tum.de/repos/isabelle/rev/aae510e9a698):
> 
> * 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
> Local_Theory.close_target.
> 
> 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.

The thread is still open, and we are now pretty close to the release.

I did not revisit this again for Isabelle2016-1. I will leave it
unchanged, under the assumption that the situation in Isabelle2016-1-RC2
is not worse than in Isabelle2016 or before.


	Makarius






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.