made SML/NJ happier

do not expose details of internal data structures for composition of BNFs

further support for nested tooltips;

tuned proofs;

refer to parent frame -- relevant for floating dockables in particular;

tuned window position to fit on screen;

tuned window position;

determine window size from content;

tuned color and font size;

close tooltip window on escape; tuned;

proper message markup for output;

some re-ordering of initialization to ensure proper formatting;

separate module Pretty_Tooltip;

refined rich tooltip options; basic tooltips without markup;

Rich_Text_Area tooltips via nested Pretty_Text_Area, based on some techniques of FoldViewer plugin;

some documentation of show_markup;

tuned proofs;

option to bypass potentially slow text overview;

tuned signature;

clarified platform dependency;

updated crontab and afp-poly settings

thread the right local theory through + reenable parallel proofs for previously problematic theories

made code more conform to rest of BNF package

more error positions;

more explicit show_type_constraint, show_sort_constraint;

recovered print translation after 'a => bool to 'a set change;

tuned;

use explicit Type.strip_sorts_dummy to suppress sort constraints in output;

printed "_ofsort" is subject to show_markup as well;

allow position constraints to coexist with 0 or 1 sort constraints; more position information in sorting error; report sorting of all type variables;