Email Gateway (Aug 19 2022 at 15:09): Email Gateway (Aug 19 2022 at 15:09):From: Lars Noschinski <noschinl@in.tum.de>
Hi,
I just noticed that the @{make_string} antiquotation seems to ignore the
ML_print_depth attribute. I.e.,
declare [[ML_print_depth=50]]
ML {* @{make_string} some_large_term *}
produces the same string as just
ML {* @{make_string} some_large_term *}
If I use PolyML.makestring instead, the attribute has the desired effect.
Is there a way to get a deeper print_depth for @{make_string} and @{print}?
-- Lars
Email Gateway (Aug 19 2022 at 15:35):From: Makarius <makarius@sketis.net>
On Wed, 30 Jul 2014, Lars Noschinski wrote:
I just noticed that the @{make_string} antiquotation seems to ignore the
ML_print_depth attribute. I.e.,declare [[ML_print_depth=50]]
ML {* @{make_string} some_large_term *}produces the same string as just
ML {* @{make_string} some_large_term *}
I refined this a bit for the next release candidate (expected on the
weekend) to make it less surprising; I also clarified the documentation
(it is a bit vague about the details, because they have changed several
times over the years).
As a general principle @{make_string} is an inlined compiler macro without
a proper run-time context. It picks up a value from the compilation
context, which might be either the one of the original function definition
or the one where it is invoked. The invocation lacks a compilation
context, if this is not inlined ML but a regular operation.
If I use PolyML.makestring instead, the attribute has the desired
effect.
The latter might be an accident due to other effects. I use raw
PolyML.makestring only as last resort within the Pure bootstrap.
Makarius
Last updated: Apr 23 2024 at 12:29 UTC