[isabelle-dev] text_fold

[Dmitriy Traytel]

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 
>>> markup
>>>  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, 
> see
> also 
> https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2013-October/msg00183.html
>
>
> 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 
> printing.
>
>
> 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 
> https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2013-October/msg00208.html

There are (commented) test cases for some of them in 
~~/src/HOL/ex/Coercion_Examples.thy . I've checked those now and they 
seem fine.

Dmitriy