proper priority for error over warning also for node_status (see 9c5220e05e04);

more direct access to persistent blobs (see also 8953d4cc060a), avoiding fragile digest lookup from later version (which might have removed unused blobs already);

always resolve symlinks for local files, e.g. relevant for ML_file to load proper source via editor instead of stored file via prover;

tuned output;

prefer non-strict Execution.print, e.g relevant for redirected ML compiler reports after error (see also e79f76a48449 and 40274e4f5ebf);

careful when calling 'Thm.proof_body_of' -- it can throw exceptions

removed unused stuff;

agree on keyword categories with ML;

more keyword categories (as in ML);

prefer dynamic ML_print_depth if context happens to be available;