[isabelle] @{make_string} and the ML_print_depth attribute


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

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