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



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


	Makarius




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