changed order of arguments to "bnf_sugar"

define selectors and discriminators

tuning

more work on BNF sugar -- up to derivation of nchotomy

more work on BNF sugar

renamed ML function for consistency

started work on datatype sugar

killed obsolete "bnf_of_typ" command

removed dead code

have "bnf_of_typ" command seal the BNF

register proofs of Isar goals, to enable recovery from unstable command states after interactive cancellation;

refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390); stretched meaning of Goal.parallel_proofs to enable future_terminal_proofs in interactive document model, despite its lack for regular forking of proofs;

some support for registering forked proofs within Proof.state, using its bottom context; tuned signature;

tuned signature;

refined status of forked goals;

proper merge of promises to avoid exponential blow-up in pathologic situations (e.g. lack of PThm wrapping);

tuned message;

discontinued old init_components script, superseded by init_components shell function as explained in README_REPOSITORY;

approximative build of pdf documents in 1 pass instead of 3;

more formal isabelle makedist from repository;

removed remains of generated material, which tends to rot;

one more round to ensure that base images are already there, without producing document output themselves;

more robust document setup;

provide polyml-5.4.1 as regular component; discontinued old-style choosefrom settings with hardwired defaults;

clarified handling of raw output messages;

no attempt to build documentation for now -- requires ML_HOME etc. which is not present here;

command 'use' is legacy;

clarified separated_chunks vs. space_explode;

more precise indentation;

modernized specifications;