Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] error mit Pretty.T


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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: Mar 29 2024 at 08:18 UTC