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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and