[isabelle-dev] Named target renovation

[Florian Haftmann]

The past days have seen a substantial renovation of the infrastructure
for named targets.  Highlights:

* 6254c51cd210 – More appropriate treatment of definitions and
abbreviations in nested local theories on top of class target.  @Andreas
This should resolve your issue from
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2014-February/msg00136.html

* 56f3351cc492 – Farewell to Named_Target.reinit, an old and odd left-over.

* 63c7b29d29ac – This was an attempt to make additional non-canonical
interpretations of classes behave more similiar to ordinary locale
interpretation esp. wrt. notation syntax.  Unfortunately, there are
still global interpretations for class order which under these
circumstances produce nonsense wrt. to _ < _ and _ <= _ and similar, so
this effect had to be reverted in 329f7f76f0a4.  It is high time to get
rid of these global interpretations of rich type classes.

* de00494fa8b3 – Since the very beginning of the class target there has
been an »educated guess« to handle constant declarations properly.  This
is now far less ad-hoc, based on identity of morphisms rather than
obscure peek criteria.  The identity of morphisms is currently
established observing the effect of morphisms on bindings and terms, and
this is still some kind of heuristic.  Future maybe will yield more
elaborate approaches.

Btw. there are still scattered ocurences of »query« operations like
Named_Target.locale_of etc. which are essentially a violation of the
local theory abstraction.  But I am optimistic that we can get rid of
those in the long run.

To get a glimpse how things have evolved over time, see here the state
of the art in Isabelle2009-2 (still without nested local theories!)

http://isabelle.in.tum.de/repos/isabelle/raw-file/35815ce9218a/src/Pure/Isar/theory_target.ML

and now the current polished version

http://isabelle.in.tum.de/repos/isabelle/raw-file/4cf607675df8/src/Pure/Isar/generic_target.ML
http://isabelle.in.tum.de/repos/isabelle/raw-file/4cf607675df8/src/Pure/Isar/named_target.ML

where any obscurity has vanished from named_target.ML (which goes back
to the ancient theory_target.ML).

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 263 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20140609/a85400e5/attachment.asc>