bnf_note_all mode for "pre_"-BNFs

separated registration of BNFs from bnf_def (BNFs are now stored only for bnf_def and (co)data commands)

tuned

beautified names

proved all upper bounds

tuned simpset

cleaner way of dealing with the set functions of sums and products

handle the general case with more than two levels of nesting when discharging induction prem prems

clean unfolding of prod and sum sets

got rid of one "auto" in induction tactic

cleaned up internal naming scheme for bnfs

more robust GUI component handlers;

more rendering;

minimal clipboard support (similar to org.lobobrowser.html.gui.HtmlBlockPanel); tuned;

output is read-only;

token marker for extended syntax styles;

pass base_snapshot to enable hyperlinks into other nodes; clarified "def" positions: refrain from renaming properties; clarified snapshot.is_output vs. output and hyperlinks;

more explicit message markup and rendering;

recover order of stacked markup;

some actual rich text markup via XML.content_markup; tuned signature;

proper separation of output messages;

some support for inital command markup; tuned signature;

more static rendering state;

Pretty_Text_Area is based on Rich_Text_Area;

renamed Text_Area_Painter to Rich_Text_Area;

tuned signature -- more general Text_Area_Painter operations;

tuned signature;

tuned signature;

tuned signature;

somewhat more general JEdit_Lib; tuned signatures;