makarius at sketis.net
Mon Feb 10 14:18:38 CET 2014
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
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.
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
> 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
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.
More information about the isabelle-dev