Re: [isabelle] error mit Pretty.T



On 22.08.2014 13:23, Makarius wrote:
> 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 here?
>
> 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})))
>   *}
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




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