David, Makarius, Thanks for the reminders. I’ll sneak a custom pretty-printer into my demo code.
Regards, Rob. > On 3 Nov 2024, at 17:39, Makarius <[email protected]> wrote: > > On 03/11/2024 18:25, David Matthews wrote: >> Originally all the printing was done at run-time but that meant that the >> type information and all the environments had to be reachable at run-time. >> That could be very large. I changed it so that a default print function was >> generated for a datatype when the datatype was declared. I have a feeling >> that the old version did indeed handle infix constructors but that could >> have been removed. > > That was 15 years ago. See the following proof in the Isabelle history: > > changeset: 33545:d8903f0002e5 > user: wenzelm > date: Tue Nov 10 13:05:35 2009 +0100 > files: src/Pure/ML-Systems/install_pp_polyml-5.3.ML > description: > home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix > status of constructors (notably $); > > https://isabelle-dev.sketis.net/rISABELLEd8903f0002e5 > > > Makarius > > _______________________________________________ > polyml mailing list > [email protected] > http://lists.inf.ed.ac.uk/mailman/listinfo/polyml _______________________________________________ polyml mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
