Re: [isabelle] @{make_string} and the ML_print_depth attribute



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




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