Re: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping



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

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

Dmitriy





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