Email Gateway (Aug 19 2022 at 15:32): Email Gateway (Aug 19 2022 at 15:32):From: Lars Noschinski <noschinl@in.tum.de>
Hi,
I just build a complex error message with "error o Pretty.string_of" and
was surprised to not see any linebreaks (for example, from
Pretty.biglist) in the output. For now, I work around it using
Pretty.string_of_margin with a fixed width. What is the correct solution
here?
-- Lars
Email Gateway (Aug 19 2022 at 15:32):From: Makarius <makarius@sketis.net>
Odd, this is done routinely and should normally work.
Here is an example:
ML {*
error (Pretty.string_of (Pretty.chunks (Display.pretty_full_theory
true @{theory})))
*}
Here is another example (via Type.appl_error):
term "x x"
What is your runtime context when you compose the Pretty.T and do the
Pretty.string_of output? There are some odd tricks that are circulated,
which circumvent the normal print_mode and other implicit context
information, which is required for the system to work properly.
Makarius
Email Gateway (Aug 19 2022 at 15:32):From: Lars Noschinski <noschinl@in.tum.de>
In contrast to what I wrote above, I used Pretty.str_of instead of
Pretty.string_of, which probably explains everything. Sorry about the noise.
-- Lars
Last updated: Nov 21 2024 at 12:39 UTC