Re: [isabelle] error mit Pretty.T
On Fri, 22 Aug 2014, Lars Noschinski wrote:
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
Odd, this is done routinely and should normally work.
Here is an example:
error (Pretty.string_of (Pretty.chunks (Display.pretty_full_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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and