>> You might still argue about syntax, e.g. having separate commands >> subscription – what is currently interpretation and subscription, not >> in free-floating contexts (as implemented in the patches). >> interpretation – only in confined contexts (locales, context begin … >> end, but not global theories any longer) without any subscription. > > That paragraph is very difficult to understand.
OK, another attempt. You can also have two distinguished commands
* subscription – interpretation with permanent subscription
* interpretation – without any subscriptions
By their very nature, interpretation would not be possible on the global
level, and subscription would not be possible in unnamed contexts.
> Note that we have one more aspect in the back-end that could help here:
> the 'private' modifier. Its meaning was not fully defined so far, but
> it could do the job:
>
> context B
> begin
>
> private interpretation A ...
> private interpretation A' ...
> private interpretation A'' ...
>
> interpretation A'' ...
>
> end
>
> Until I manage to get 'private' as command modifier into the toplevel
> interpreter, we can tentatively use 'private_interpretation'.
So the proposal would be to have two commands
* interpretation (»subscription« from above)
* private_interpretation (»interpretation« from above)
Until now I have been thinking about »private« to be a certain name
space policy. I don't forsee how exactly this relates to subscriptions.
Maybe it is a different thing. For this reason I would prefer my own
naming scheme at the moment.
Cheers,
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 [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
