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



Hi Makarius,

> On 10 Nov 2016, at 13:50, Makarius <makarius at sketis.net> wrote:
> 
> 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.

sure, this is fine. We have a workaround not to rely on configuration options (but instead pass a Boolean flag around) for the problem I reported originally anyway.

Dmitriy



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