Email Gateway (Aug 19 2022 at 11:15): Email Gateway (Aug 19 2022 at 11:15):From: Steffen Juilf Smolka <steffen.smolka@in.tum.de>
Hi,
what is the difference between the normal and the global pretty printing functions defined in syntax.ML?
Best regards,
Steffen
Email Gateway (Aug 19 2022 at 11:18):From: Makarius <makarius@sketis.net>
Here is a relevant quotation from the "implementation" manual:
\item The name component @{ML_text global} means that this works
with the background theory instead of the regular local context
(\secref{sec:context}), sometimes for historical reasons, sometimes
due a genuine lack of locality of the concept involved, sometimes as
a fall-back for the lack of a proper context in the application
code. Whenever there is a non-global variant available, the
application should be migrated to use it with a proper local
context.
Under normal circumstances you don't use global things, other than for
historical reasons, or very special situations.
Sometimes people think that the normal local Proof.context is too complex,
and should thus be avoided by falling back on good-old global stuff, but
that is the wrong approach. It requires quite some expertise on both
local vs. global operations to use old global stuff in the proper way.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC