[isabelle-dev] Interpretation in arbitrary targets.
florian.haftmann at informatik.tu-muenchen.de
Wed Mar 27 12:42:47 CET 2013
>> 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
> private interpretation A ...
> private interpretation A' ...
> private interpretation A'' ...
> interpretation A'' ...
> 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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 261 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev