traytel at in.tum.de
Mon Feb 10 14:47:13 CET 2014
Am 10.02.2014 14:18, schrieb Makarius:
> On Mon, 25 Nov 2013, Dmitriy Traytel wrote:
>> Am 23.11.2013 19:42, schrieb Makarius:
>>> On Mon, 28 Oct 2013, Dmitriy Traytel wrote:
>>> > Concerning the error messages: at least you should always get >
>>> strictly more information than without coercion inference (i.e. the
>>> > error message of the standard type-inference will always come
>>> first, > only then coercion inference will give additional hints).
>>> Of course, > the additional information can be distracting---maybe
>>> it should be > hidden in a popup or so).
>>> Concerning the "popup or so" you could experiment with
>>> Pretty.text_fold (although the fold will be always open by default in
>>> currently published Isabelle versions).
>>> The Isabelle Pretty module started out as implementation of
>>> Oppen-style pretty-printing by Larry Paulson, but it has acquired more
>>> and more logical markup facilities over the years (e.g. Pretty.markup,
>>> Pretty.paragraph, Pretty.item).
>>> The full potential of this is still unused. (Display of advanced
>>> requires a proper PIDE front-end.)
>> Thanks for the hint. There result of my experiments are in the
>> development repository (2bbcbf8cf47e).
> This thread that originated from isabelle-users is still somehow open,
> In Isabelle/35354009ca25 I have sorted out some misunterstandings
> about Markup and Pretty.
> Pretty.text_fold is fine if you assemble pretty trees, but having
> already formatted strings means you can't go through a pretty tree
> again: Pretty.str assumes an atomic argument. (There used to be a
> mostly forgotten ML naming convention, to use "str" for unformatting
> strings and "string" for formatted ones, cf. Pretty.str vs.
> Pretty.str_of vs. Pretty.string_of.)
I see. Thanks for repairing this.
> The reason why that API mismatch was not immediately detected is that
> Isabelle/Scala does its own rendering of pretty trees, from the
> overall output produced by the prover. This occasionally hides
> Isabelle/ML programming mistakes concerning Pretty.T, until someone
> uses a historical Isabelle front-end, or does Isabelle latex pretty
> Using Markup.text_fold and already formatted strings in 35354009ca25
> makes the situation formally more correct, and simpler. What I can't
> test here are all the individual error messages, because I don't know
> how to provoke them. I've merely done a sanity check with the
> original example from
There are (commented) test cases for some of them in
~~/src/HOL/ex/Coercion_Examples.thy . I've checked those now and they
More information about the isabelle-dev