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 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})))
  *}

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




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