>>> This does not exhibit itself until the compromised locale context is >>> (re-)entered, and I think this is not desirable. My first >>> spontaneous thought is that strictness should not apply during the >>> initialisation of a locale context. >> >> I wouldn't want to add special treatment for this. Currently we can >> only ensure that a locale is intact by visiting its context. It would >> be better if integrity checking could be done in an incremental >> fashion. But that would require much more sophistication. > > Or is that actually an answer to the problem above: assuming that > re-init is fast, it could be done more often to check the name space, > but its transformed results remain unchecked.
My thought are also going in that direction of »early checking«, e.g.
getting feedback when something is going to be compromised rather at a
later (unrelated) re-entering of a locale context.
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
