Re: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping
Am 23.11.2013 19:42, schrieb Makarius:
Thanks for the hint. There result of my experiments are in the
development repository (2bbcbf8cf47e).
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,
The full potential of this is still unused. (Display of advanced
markup requires a proper PIDE front-end.)
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and