Re: [isabelle] Calling Mixfix.pretty_mixfix
On Mon, 7 Mar 2011, John Munroe wrote:
I'm trying to call Mixfix.pretty_mixfix in ML mode, but it complains
about Mixfix being not declared. Does anyone know why? In fact, I get
the error for all structures in Pure/Syntax. Is it somehow not included
in the image? Is there a setting somewhere I need to change?
It is available as Syntax.pretty_mixfix
As a general principle, the structures contributing to the "Isabelle
Syntax module" are built up in stages, and only part of the content ends
up as publicly accessible via the main interface of structure Syntax.
You essentially see here remains of older experiments with the ML module
system from the early 1990-ies (back then we even had many vacous functors
around the code). Nonetheless, the Syntax structures are in a clean
state, i.e. the intentionally public things are public (despite the slight
onconvenience in the source arrangement).
This archive was generated by a fusion of
Pipermail (Mailman edition) and