support for begin/end matching;

proper token kind;

added option jedit_structure_limit; tuned signature;

some structure matching, based on line token iterators;

support for structure matching; misc tuning;

tuned rendering;

back to alternative fold painter, despite f03a9c57760a -- gutter painter seems to have changed in the meantime;

tuned;

update_cartouches;

clarified tree root;

tuned spacing;

clarified verbatim line breaks, e.g. relevant for Implementation mldecls;

turn even into an abbreviation

update documentation for 'size_o_map'

rename 'size_o_map' to 'size_gen_o_map'

document 'size_gen'

generate 'size_gen' for datatypes

document 'map_o_corec'

generate 'map_o_corec' for (co)datatypes * * * document 'map_o_corec'

move documentation of 'rec_o_map'

move theorem 'rec_o_map' * * * move documentation of 'rec_o_map'

warn for not fully mutually (co)recursive types

add transfer rule for set_pmf

add tendsto_const and tendsto_ident_at as simp and intro rules

tuned spacing;

avoid odd ligatures;

more accurate approximation of AST;

tuned exposition of {* ... *};