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).


	Makarius





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