Re: [isabelle] "global" pretty printing

On Tue, 11 Jun 2013, Steffen Juilf Smolka wrote:

Hi, what is the difference between the normal and the global pretty printing functions defined in syntax.ML?

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

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.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.