Email Gateway (Aug 18 2022 at 17:20): Email Gateway (Aug 18 2022 at 17:20):From: John Munroe <munddr@gmail.com>
Hi,
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?
Any help will be greatly useful. Thanks.
John
Email Gateway (Aug 18 2022 at 17:20):From: Makarius <makarius@sketis.net>
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
Last updated: Oct 31 2025 at 20:23 UTC