[isabelle-dev] Afterthoughts on Local_Theory.subtarget_result

[Makarius]

On 22/01/2019 22:24, Florian Haftmann wrote:
> 
> as of 82f57315cade (followed-up by AFP bf62184), the still occasionally
> seen Local_Theory.reset invocations are gone, conveniently replaced by
> Local_Theory.subtarget_result.

This looks clean and canonical. At least we have Local_Theory.reset out
of the way in visible Isabelle/ML tool implementations: it is still
present inside Local_Theory.close_target, though.

I wonder what happens when that is removed: presumably it requires a lot
of fine-tuning to make everything work again without that hidden reset.


	Makarius

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20190131/f1170353/attachment.sig>