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
