allow to remove print functions; tuned signature;

clarified Command.print: update old prints here;

produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);

tuned;

tuned proofs;

more formal type assign_update: avoid duplicate results and redundant update of global State.execs;

tuned message;

tuned signature -- NB: Command.read is actually part of Command.eval;

tuned protocol terminology; tuned signature;

tuned;

allow whitespace in file names;

tuned;

more direct interleaving of eval/print and update/execution -- refrain from crude manipulation of max_threads;

allow worker guest threads, which participate actively in future joins, but are outside thread accounting;

made SML/NJ happy

completely rewrote SH compress; added two parameters for experimentation/fine grained control

moved code -> easier debugging

tuned proofs

some support for Cygwin;

reduced number of old manuals: chapter HOL is back again to the Logics manual by Larry;

tuned signature;

discontinued obsolete "isabelle print";

discontinued command 'print_drafts';

some attempts to avoid sandwiching of actions stemming from single ESCAPE key event, to avoid potential conflict with ongoing text selection;

removed pointless / outdated keywords, superseded by specific Token_Markup.Marker;

tuned comments;

Func -> Func_option, Ffunc -> Func (avoids dependence of codatatypes on the option type)

tuned spelling