[isabelle-dev] text_fold

[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.)

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


> It would be nice if the default status (folded or not) could be 
> indicated by a parameter to Pretty.text_fold (and respected by the 
> front-end).

That is an open thread from before Christmas (2012, not 2013).  It would 
require some work in the Pretty_Text_Area of Isabelle/jEdit, to combine 
some GUI "state" with the formal document content, in ways I can't foresee 
at the moment.  It will probably turn out again as some tinkering with 
Command.Results in Isabelle/Scala.


 	Makarius