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



On Mon, 25 Nov 2013, Dmitriy Traytel wrote:

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

I will take a look soon, and continue this thread on isabelle-dev.


	Makarius




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